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

changeset 1123:256a3ba634f6

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 Wed, 04 Jan 2023 11:21:55 +0900
parents 1c7474446754
children d122d0c1b094
files src/BAlgbra.agda src/Topology.agda
diffstat 2 files changed, 26 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgbra.agda	Wed Jan 04 09:39:25 2023 +0900
+++ b/src/BAlgbra.agda	Wed Jan 04 11:21:55 2023 +0900
@@ -53,6 +53,13 @@
 ¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
 ¬∅∋ {x} = ¬x<0
 
+L＼L=0 : { L  : HOD  } → L ＼ L ≡ od∅ 
+L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← =  lem1 } ) where
+    lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
+    lem0 {x} ⟪ lx , ¬lx ⟫ = ⊥-elim (¬lx lx)
+    lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
+    lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
+
 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
      ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
--- a/src/Topology.agda	Wed Jan 04 09:39:25 2023 +0900
+++ b/src/Topology.agda	Wed Jan 04 11:21:55 2023 +0900
@@ -50,10 +50,11 @@
    cs⊆L :  {x : HOD} → CS ∋ x → x ⊆ L
    cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy )
    CS∋L : CS ∋ L
-   CS∋L = ⟪ ? , ? ⟫
+   CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x)  , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅  ⟫ where
+        lem0 : L ＼ * (& L) ≡ od∅
+        lem0 = subst (λ k → L ＼ k  ≡ od∅) (sym *iso) L＼L=0
 --- we may add
 --     OS∋L   :  OS ∋ L
---     OS∋od∅ :  OS ∋ od∅
 
 open Topology
 
@@ -61,6 +62,11 @@
 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x  } 
   ; odmax = & L ; <odmax = ? }
 
+ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L
+ClL {L} top {f} =  ==→o≡ ( record { eq→ = λ {x} ic 
+        → subst (λ k → odef k x) *iso (ic (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
+    ; eq← =  λ {x} lx c cs l⊆c → l⊆c lx } )
+
 -- Subbase P
 --   A set of countable intersection of P will be a base (x ix an element of the base)
 
@@ -290,29 +296,30 @@
 -- FIP is UFL
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
-   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FL uf
-FIP→UFLP {P} TP fip {L} LP F FL uf = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf
+FIP→UFLP {P} TP fip {L} LP F FP uf = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
     where
+      fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
+      fip03 {z} fz {x} zx = LP ( f⊆L F fz ) x (subst (λ k → odef k x) (sym *iso) zx  )
       CF : Ordinal
       CF = & ( Replace' (filter F) (λ z fz → Cl TP z (fip03 fz)) ) where
-         fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
-         fip03 {z} fz {x} zx with LP ( f⊆L F fz )
-         ... | pw = pw x (subst (λ k → odef k x) (sym *iso) zx  )
-      CFP : * CF ∋ P  -- filter F ∋ P
-      CFP = ?
+      CFP : * CF ∋ P  -- filter F ∋ P and Cl P ≡ P
+      CFP = subst₂ (λ j k → odef j k) (sym *iso) refl record { z = & P ; az = FP ; x=ψz =  cong (&) fip04 }  where
+           fip04 : P ≡ (Cl TP (* (& P)) (fip03 (subst (odef (filter F)) (sym &iso) FP)))
+           fip04 =  ==→o≡ ( record { eq→ = ? ;  eq← =  ?  } )
       fip00 : * CF ⊆ CS TP -- replaced
       fip00 = ?
       fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x
       fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅
       fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ?
-      fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 ? fip01) → * o ⊆ filter F
+      fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 CFP fip01) → * o ⊆ filter F
       fip02 {p} oo ol = ? where
-         fip04 : odef ? (FIP.limit fip fip00 ? fip01) 
+         fip04 : odef ? (FIP.limit fip fip00 CFP fip01) 
          fip04 = FIP.is-limit fip fip00 CFP fip01 ?
 
 
 UFLP→FIP : {P : HOD} (TP : Topology P) →
-   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F ? uf ) → FIP TP
+   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf ) → FIP TP
 UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? }
 
 -- Product of UFL has limit point (Tychonoff)