From e956eab1116ae48a298e3c6701f93178e53ab24f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 22 Sep 2009 12:05:37 +0000
Subject: [PATCH] ...

---
 .../software/matita/nlibrary/topology/igft.ma | 95 ++++++++++++++-----
 1 file changed, 70 insertions(+), 25 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 9d61e0af6..7f4f5e359 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -122,6 +122,12 @@ nrecord nAx : Type[2] ≝ {
   nd: ∀a:nS. ∀i:nI a. nD a i → nS
 }.
 
+(*
+TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
+
+a = b → I a = I b
+*)
+
 notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
 notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.
 
@@ -139,7 +145,6 @@ notation "𝐈𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with preced
 
 interpretation "image" 'Im a i = (image ? a i).
 
-(*
 ndefinition Ax_of_nAx : nAx → Ax.
 #A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
 nqed.
@@ -155,7 +160,6 @@ ndefinition nAx_of_Ax : Ax → nAx.
 ##| #a; #i; *; #x; #_; napply x;
 ##]
 nqed.
-*)
 
 ninductive Ord (A : nAx) : Type[0] ≝ 
  | oO : Ord A
@@ -174,24 +178,6 @@ nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
   | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un} 
   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
   
-naxiom XXX : False.  
-  
-ndefinition qp_famU : ∀A:nAx.∀U:qpowerclass A.∀x:Ord A.qpowerclass A ≝ 
-  λA,U,x.?. 
-@ (famU ? (pc ? U) x); nelim x;
-##[ #a; #b; #E; nnormalize; @; #H; ##[ napply (. E^-1‡#); napply H; ##| napply (. E‡#); napply H; ##]  
-##| #o; #IH; #a; #b; #E; @; nnormalize; *; #H;
-    ##[##1,3: @1; nlapply (IH … E); *; #G; #G'; 
-              ##[ napply G | napply G'] nassumption;
-    ##|##2,4: @2; ncases H; #i_a; #H_ia; @;
- nelim XXX; ##]
-##| nelim XXX; 
-##]
-nqed.
-
-unification hint 0 ≔ 
-  A,U,x; UU ≟ (pc ? U) ⊢ pc ? (qp_famU A U x) ≡ famU A UU x.
-
 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
 notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
 
@@ -221,9 +207,6 @@ naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.
 naxiom setoidification :
   ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
 
-alias symbol "covers" = "new covers set".
-alias symbol "covers" = "new covers".
-alias symbol "covers" = "new covers set".
 alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
 alias symbol "covers" = "new covers".
@@ -235,7 +218,8 @@ ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
 ncases (AC … H'); #f; #Hf;
 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
   ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
-@ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd; napply (setoidification … Hd); napply Hf';
+@ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd; 
+napply (setoidification … Hd); napply Hf';
 nqed.
 
 (* move away *)
@@ -252,5 +236,66 @@ nelim o;
     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
 nqed.
+
+nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
+  match x with
+  [ oO ⇒ F
+  | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo } 
+  | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
+  ].
+
+interpretation "famF" 'famU U x = (famF ? U x).
+
+ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.
+
+interpretation "fished new fish" 'fished U = (ord_fished ? U).
+interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
+
+ntheorem new_fish_antirefl:
+ ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+#A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
+nqed.
+
+nlemma co_ord_subset:
+ ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
+#A; #F; #a; #i; #f; #j; #x; #H; napply H;
+nqed.
+
+naxiom AC_dual : 
+  ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
+
+
+ntheorem new_fish_compatible: 
+ ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
+#A; #F; #a; #aF; #i; nnormalize;
+napply AC_dual; #f;
+nlapply (aF (Λf+1)); #aLf;
+nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
+ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
+  ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
+napply aLf';
+nqed.
+
+(* move away *)
+nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
+#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
+nqed.
+
+nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
+#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
+nqed. 
  
- 
\ No newline at end of file
+ntheorem max_new_fished: 
+  ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+#A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
+nchange with (G ⊆ F⎽o);
+nelim o;
+##[ napply GF;
+##| #p; #IH; napply (subseteq_intersection_r … IH);
+    #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
+    @d; napply IH; napply (setoidification … Ed^-1); napply cG;   
+##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
+    #b; #Hb; #d; napply (Hf d); napply Hb;
+##]
+nqed.
+
-- 
2.39.2