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

changeset 1204:4d894c166762

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 03 Mar 2023 08:37:02 +0800
parents 2f09ce1dd2a1
children 83ac320583f8
files src/Tychonoff.agda
diffstat 1 files changed, 18 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Thu Mar 02 18:03:04 2023 +0900
+++ b/src/Tychonoff.agda	Fri Mar 03 08:37:02 2023 +0800
@@ -85,7 +85,7 @@
            * o∅ ≡⟨  o∅≡od∅ ⟩
            od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
    ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  ? } where
+... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  uf01 } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
@@ -94,25 +94,20 @@
      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
-     nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
-     nc {X} CSX fip with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where
+     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) )
-     ... | tri≈ ¬a b ¬c = od∅
-     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-     N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc CSX fip) )
-     N∋nc {X} CSX fip with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = record { b = ? ; x =  ? ;  b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where
+     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
           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))) ) 
-     ... | tri≈ ¬a b ¬c = ? -- od∅
-     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      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∅
@@ -156,48 +151,30 @@
      maxf {X} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} CSX fp =  MaximumFilter.mf (maxf CSX fp) 
-     ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
-     ultraf {X} CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
+     ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
+     ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
      --
      -- so i has a limit as a limit of UIP
      --
      limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
      limit {X} CSX fp with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
-     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
-           * X ≡⟨ cong (*) (sym 0=X) ⟩
-           * o∅ ≡⟨  o∅≡od∅ ⟩
-           od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
+     ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))
+     ... | tri≈ ¬a 0=X ¬c = o∅ 
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-     uf02 : {X v  : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
+     uf02 : {X v  : Ordinal} → (0<X : o∅ o< X)  → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
         → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
-     uf02 {X} {v} CSX fp nei {x} vx with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf CSX fp)) nei vx
-     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
-           * X ≡⟨ cong (*) (sym 0=X) ⟩
-           * o∅ ≡⟨  o∅≡od∅ ⟩
-           od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
+     uf02 {X} {v} 0<X CSX fp nei {x} vx with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) nei vx
+     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a 0<X )
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      --
      -- the limit is an limit of entire elements of X
      --
      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 ODC.∋-p O (* x) (* (limit CSX fp))
-     ... | yes y = subst (λ k → odef (* x) k) &iso y
-     ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 )  where
-         uf03 : OS TP ∋  ( P ＼ (* x))
-         uf03 = ?
-         uf05 : odef ( P ＼ (* x)) (limit CSX fp)
-         uf05 = ⟪  ? , subst (λ k → ¬ odef (* x) k) ?  nxl ⟫
-         uf04 : Neighbor TP (limit CSX fp) (& ( P ＼ (* (limit CSX fp))))
-         uf04 = record { u = & ( P ＼ (* x)) ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ? }
-         uf07 : odef (filter (mf CSX fp)) x
-         uf07 = ?
-         uf06 : odef (filter (mf CSX fp)) (& ( P ＼ (* x)) )
-         uf06 = ?
-         uf08 : (filter (mf CSX fp)) ∋ od∅
-         uf08 = ?
-            
+     uf01 {X} CSX fp {x} xx with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = ?
+     ... | tri≈ ¬a 0=X ¬c = ?
+     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF