Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Topology.agda @ 1123:256a3ba634f6
...
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) |