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

comparison src/Topology.agda @ 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
comparison
equal deleted inserted replaced
1122:1c7474446754 1123:256a3ba634f6
48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L 48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L
49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) 49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy )
50 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L 50 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L
51 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) 51 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy )
52 CS∋L : CS ∋ L 52 CS∋L : CS ∋ L
53 CS∋L = ⟪ ? , ? ⟫ 53 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where
54 lem0 : L ＼ * (& L) ≡ od∅
55 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0
54 --- we may add 56 --- we may add
55 -- OS∋L : OS ∋ L 57 -- OS∋L : OS ∋ L
56 -- OS∋od∅ : OS ∋ od∅
57 58
58 open Topology 59 open Topology
59 60
60 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD 61 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD
61 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x } 62 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x }
62 ; odmax = & L ; <odmax = ? } 63 ; odmax = & L ; <odmax = ? }
64
65 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L
66 ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic
67 → subst (λ k → odef k x) *iso (ic (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
68 ; eq← = λ {x} lx c cs l⊆c → l⊆c lx } )
63 69
64 -- Subbase P 70 -- Subbase P
65 -- A set of countable intersection of P will be a base (x ix an element of the base) 71 -- A set of countable intersection of P will be a base (x ix an element of the base)
66 72
67 data Subbase (P : HOD) : Ordinal → Set n where 73 data Subbase (P : HOD) : Ordinal → Set n where
288 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F 294 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
289 295
290 -- FIP is UFL 296 -- FIP is UFL
291 297
292 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP 298 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
293 → {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 299 → {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
294 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 } 300 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 }
295 where 301 where
302 fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
303 fip03 {z} fz {x} zx = LP ( f⊆L F fz ) x (subst (λ k → odef k x) (sym *iso) zx )
296 CF : Ordinal 304 CF : Ordinal
297 CF = & ( Replace' (filter F) (λ z fz → Cl TP z (fip03 fz)) ) where 305 CF = & ( Replace' (filter F) (λ z fz → Cl TP z (fip03 fz)) ) where
298 fip03 : {z : HOD} → filter F ∋ z → z ⊆ P 306 CFP : * CF ∋ P -- filter F ∋ P and Cl P ≡ P
299 fip03 {z} fz {x} zx with LP ( f⊆L F fz ) 307 CFP = subst₂ (λ j k → odef j k) (sym *iso) refl record { z = & P ; az = FP ; x=ψz = cong (&) fip04 } where
300 ... | pw = pw x (subst (λ k → odef k x) (sym *iso) zx ) 308 fip04 : P ≡ (Cl TP (* (& P)) (fip03 (subst (odef (filter F)) (sym &iso) FP)))
301 CFP : * CF ∋ P -- filter F ∋ P 309 fip04 = ==→o≡ ( record { eq→ = ? ; eq← = ? } )
302 CFP = ?
303 fip00 : * CF ⊆ CS TP -- replaced 310 fip00 : * CF ⊆ CS TP -- replaced
304 fip00 = ? 311 fip00 = ?
305 fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x 312 fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x
306 fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅ 313 fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅
307 fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ? 314 fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ?
308 fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 ? fip01) → * o ⊆ filter F 315 fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 CFP fip01) → * o ⊆ filter F
309 fip02 {p} oo ol = ? where 316 fip02 {p} oo ol = ? where
310 fip04 : odef ? (FIP.limit fip fip00 ? fip01) 317 fip04 : odef ? (FIP.limit fip fip00 CFP fip01)
311 fip04 = FIP.is-limit fip fip00 CFP fip01 ? 318 fip04 = FIP.is-limit fip fip00 CFP fip01 ?
312 319
313 320
314 UFLP→FIP : {P : HOD} (TP : Topology P) → 321 UFLP→FIP : {P : HOD} (TP : Topology P) →
315 ( {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 322 ( {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
316 UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? } 323 UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? }
317 324
318 -- Product of UFL has limit point (Tychonoff) 325 -- Product of UFL has limit point (Tychonoff)
319 326
320 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) 327 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ)