Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1205:83ac320583f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 03 Mar 2023 10:42:58 +0800
parents 4d894c166762
children 2c7fb857f144
files src/Tychonoff.agda
diffstat 1 files changed, 17 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Fri Mar 03 08:37:02 2023 +0800
+++ b/src/Tychonoff.agda	Fri Mar 03 10:42:58 2023 +0800
@@ -43,7 +43,7 @@
 -- FIP is UFL
 
 -- filter Base
-record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
+record FBase (P : HOD ) (X : Ordinal ) (u : Ordinal) : Set n where
    field
        b x : Ordinal
        b⊆X : * b ⊆ * X
@@ -93,21 +93,20 @@
         ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt))  }
      N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
      N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
-     -- filter base is not empty
+     -- filter base is not empty necessary for generating ultra filter
      nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
-     nc {X} 0<X CSX fip = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where
-          e : HOD  -- we have an element of X
-          e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
-          Xe : odef (* X) (& e)
-          Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
+     nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X
      N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) 
         → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
-     N∋nc {X} 0<X CSX fip = record { b = ? ; x =  ? ;  b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where
+     N∋nc {X} 0<X CSX fip = record { b = X ; x =  & e ;  b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where
           e : HOD  -- we have an element of X
           e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           Xe : odef (* X) (& e)
           Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) 
+          nn02 : * (& (nc 0<X CSX fip)) ⊆ P
+          nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
+
      0<PP : o∅ o< & (Power P)
      0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
           nn00 : odef (Power P) o∅
@@ -172,8 +171,16 @@
      --
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
      uf01 {X} CSX fp {x} xx with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = ?
-     ... | tri≈ ¬a 0=X ¬c = ?
+     ... | tri< 0<X ¬b ¬c = uf02 0<X CSX fp uf03 uf05 where
+        uf04 : Ordinal 
+        uf04 = ?
+        uf06 : Ordinal 
+        uf06 = ?
+        uf05 : odef (* uf04) uf06
+        uf05 = ?
+        uf03 : Neighbor TP (limit CSX fp) uf04
+        uf03 = record { u = ? ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ?  } 
+     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx )))
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP