X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=56a8c4120b802e3b65dc73f14417820c22d58855;hb=e189bde1e0a562e8689ff41d55d392431609e749;hp=41c0d5c53cb2253fe4a9ea2e0deca0c275d89529;hpb=102f828310b347680407c0a5b51084bfaa88f458;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 41c0d5c53..56a8c4120 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -109,6 +109,24 @@ theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a 
        assumption]]
 qed.
 
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+  (∀a:A. a ∈ U → P a) →
+   (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+     ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+  [ intros 2; simplify; apply H; assumption
+  | intros;
+    simplify in H4 ⊢ %;
+    apply H1;
+     [ apply (C ? a1 j);
+     | autobatch;
+     | assumption;
+     | assumption]]
+qed.
+
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;
  cases H;
@@ -158,13 +176,9 @@ qed.
 
 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
 
-notation "↑a" with precedence 80 for @{ 'uparrow $a }.
-
 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 
-definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
-
-notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
 
 interpretation "downarrow" 'downarrow a = (downarrow _ a).
 
@@ -174,6 +188,5 @@ interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
 
 record convergent_generated_topology : Type ≝
  { AA:> axiom_set;
-   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
  }.
-