...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 3e9e359d5f01109f9743e7e0f0f7d27f1c303ee3..9d61e0af603680e0ddbbc5eaf8204b549a5c35f4 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -130,6 +130,7 @@ notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence
 
 interpretation "D" 'D a i = (nD ? a i).
 interpretation "d" 'd a i j = (nd ? a i j).
+interpretation "new I" 'I a = (nI ? a).
 
 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
 
@@ -138,6 +139,7 @@ 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.
@@ -153,16 +155,102 @@ ndefinition nAx_of_Ax : Ax → nAx.
 ##| #a; #i; *; #x; #_; napply x;
 ##]
 nqed.
+*)
 
-ninductive ord (A : nAx) : Type[0] ≝ 
- | oO : ord A
- | oS : ord A → ord A
- | oL : ∀a:A.∀i.∀f:𝐃 a i → ord A. ord A.
+ninductive Ord (A : nAx) : Type[0] ≝ 
+ | oO : Ord A
+ | oS : Ord A → Ord A
+ | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
 
-nlet rec famU (A : nAx) (U : Ω^A) (x : ord A) on x : Ω^A ≝ 
+notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 50 for @{'oS $x }.
+
+interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
+interpretation "ordinals Succ" 'oS x = (oS ? x).
+
+nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ 
   match x with
   [ oO ⇒ U
-  | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.∀j:𝐃 x i.𝐝 x i j ∈ Un} 
+  | 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) } ].
   
-ndefinition ord_coverage ≝ λA,U.{ y | ∃x:ord A. y ∈ famU ? U x }.   
+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 }.
+
+interpretation "famU" 'famU U x = (famU ? U x).
+  
+ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
+
+ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
+  ∀y.y ∈ C → y ∈ c A U.
+
+interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
+interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
+interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
+
+ntheorem new_coverage_reflexive:
+  ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+#A; #U; #a; #H; @ (oO A); napply H;
+nqed.
+
+nlemma ord_subset:
+  ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
+#A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
+nqed.
+
+naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
+
+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".
+ntheorem new_coverage_infinity:
+  ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
+#A; #U; #a; *; #i; #H; nnormalize in H;
+ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
+  #y; napply H; @ y; napply #; ##] #H'; 
+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';
+nqed.
+
+(* move away *)
+nlemma subseteq_union: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
+#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
+nqed. 
+
+nlemma new_coverage_min :  
+  ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
+#A; #U; #V; #HUV; #Im;  #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
+nelim o;
+##[ #b; #bU0; napply HUV; napply bU0;
+##| #p; #IH; napply subseteq_union; ##[ nassumption; ##]
+    #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
+##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
+nqed.
+ 
+ 
\ No newline at end of file