...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 04f4be9c706d8df25238c9edfe3d625cf3380838..9bff8502fba897a233caa3f7f8148c54a8fc190e 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -53,6 +53,60 @@ nlet corec fish_rec (A:axiom_set) (U: Ω^A)
 ##]
 nqed.
 
+notation "◃U" non associative with precedence 55
+for @{ 'coverage $U }.
+
+ndefinition coverage : ∀A:axiom_set.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
+
+interpretation "coverage cover" 'coverage U = (coverage ? U).
+
+ndefinition cover_equation : ∀A:axiom_set.∀U,X:Ω^A.CProp[0] ≝  λA,U,X. 
+  ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:I ? a.∀y.y ∈ C ? a i → y ∈ X).  
+
+ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
+#A; #U; #a; @; #H;
+##[ nelim H; #b; (* manca clear *)
+    ##[ #bU; @1; nassumption;
+    ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
+        ##[ #E; @; napply E;
+        ##| #_; napply CaiU; nassumption; ##] ##]
+##| ncases H; ##[ #E; @; nassumption]
+    *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
+##]
+nqed. 
+
+ntheorem coverage_min_cover_equation : ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
+#A; #U; #W; #H; #a; #aU; nelim aU; #b;
+##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
+##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
+##]
+nqed.
+
+notation "⋉F" non associative with precedence 55
+for @{ 'fished $F }.
+
+ndefinition fished : ∀A:axiom_set.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.
+
+interpretation "fished fish" 'fished F = (fished ? F).
+
+ndefinition fish_equation : ∀A:axiom_set.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
+  ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:I ? a.∃y.y ∈ C ? a i ∧ y ∈ X. 
+  
+ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
+#A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
+##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
+    napply cF;  
+##| #aF; #H1; @ aF; napply H1;
+##]
+nqed.
+
+ntheorem fised_min_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
+#A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
+#b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; 
+nqed. 
+
+STOP
+
 (*
 alias symbol "covers" (instance 0) = "covers".
 alias symbol "covers" (instance 2) = "covers".
@@ -84,6 +138,9 @@ nelim aU;
 ##]
 nqed.
 
+
+
+
 STOP
 
 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.