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

changeset 1209:09e4b32ece2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Mar 2023 21:31:12 +0900
parents 151f4c971a50
children 806109d79562
files src/Tychonoff.agda
diffstat 1 files changed, 19 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Fri Mar 03 19:44:29 2023 +0900
+++ b/src/Tychonoff.agda	Fri Mar 03 21:31:12 2023 +0900
@@ -213,7 +213,20 @@
 
 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
-FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
+FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 
+   ; P∋limit = ufl10 ; is-limit = ufl00 } where
+     F∋P : odef (filter F) (& P)
+     F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) )  (λ z az → proj1 (subst (λ k → odef k z) *iso az ) )
+     ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp )
+     ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
+         fl20 :  (P ＼ Ord o∅) =h=  P
+         fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  } 
+     0<P : o∅ o< & P
+     0<P with trio< o∅ (& P)
+     ... | tri< a ¬b ¬c = a
+     ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋P) )
+     ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+
      --
      -- take closure of given filter elements
      --
@@ -251,6 +264,10 @@
            o∅ ≡⟨ sym ord-od∅ ⟩
            & od∅  ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) ))  where open ≡-Reasoning
         ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+     ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01)
+     ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11  where
+         ufl11 : odef (* (& CF)) (& P)
+         ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az  = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP)))   }  
      --
      -- so we have a limit
      --
@@ -264,7 +281,7 @@
      ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅  -- because limit is in CF 
      ufl03 {f} {v} ff nei fv=0 = ?
      pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
-     pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = v⊆P ?
+     pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = ?
      ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 
      ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
      ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv