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

comparison src/Topology.agda @ 1160:2479884b35b2

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, 20 Jan 2023 17:02:09 +0900
parents adba530ce1f0
children b45925515f77
comparison
equal deleted inserted replaced
1159:adba530ce1f0 1160:2479884b35b2
39 OS : HOD 39 OS : HOD
40 OS⊆PL : OS ⊆ Power L 40 OS⊆PL : OS ⊆ Power L
41 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) 41 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
42 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P 42 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P
43 OS∋od∅ : OS ∋ od∅ 43 OS∋od∅ : OS ∋ od∅
44 --- we may add
45 -- OS∋L : OS ∋ L
44 -- closed Set 46 -- closed Set
45 CS : HOD 47 CS : HOD
46 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where 48 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where
47 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L ＼ * y)) → y o< osuc (& L) 49 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L ＼ * y)) → y o< osuc (& L)
48 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx )) 50 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx ))
54 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where 56 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where
55 lem0 : L ＼ * (& L) ≡ od∅ 57 lem0 : L ＼ * (& L) ≡ od∅
56 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0 58 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0
57 CS⊆PL : CS ⊆ Power L 59 CS⊆PL : CS ⊆ Power L
58 CS⊆PL {x} Cx y xy = proj1 Cx xy 60 CS⊆PL {x} Cx y xy = proj1 Cx xy
59 --- we may add 61 P＼CS=OS : {cs : HOD} → CS ∋ cs → OS ∋ ( L ＼ cs )
60 -- OS∋L : OS ∋ L 62 P＼CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (cong (λ k → & ( L ＼ k)) *iso) olcs
63 P＼OS=CS : {cs : HOD} → OS ∋ cs → CS ∋ ( L ＼ cs )
64 P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1
65 , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos ⟫
61 66
62 open Topology 67 open Topology
63 68
64 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD 69 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD
65 Cl {L} top A A⊆L = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } 70 Cl {L} top A A⊆L = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) }
67 72
68 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L 73 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L
69 ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic 74 ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic
70 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) 75 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
71 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) 76 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
77
78 record NAO {L : HOD} (top : Topology L) (A : HOD) (A⊆L : A ⊆ L) (x : Ordinal) : Set n where
79 field
80 ox : odef (OS top) x
81 na : ¬ ( A ⊆ * x)
82
83 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → (A⊆L : A ⊆ L) → CS top ∋ Cl top A A⊆L
84 CS∋Cl {L} top A A⊆L = ⟪ (λ {x} cx → proj1 ( subst (λ k → odef k x) *iso cx )) , ? ⟫ where
85 NCl : HOD
86 NCl = record { od = record { def = λ x → NAO top A A⊆L x } ; odmax = & (OS top) ; <odmax = λ lt → odef< (NAO.ox lt) }
87 NCl⊂OS : NCl ⊂ OS top
88 NCl⊂OS = ⟪ ? , ? ⟫
89 ccl00 : (L ＼ (Cl top A A⊆L)) ≡ Union NCl
90 ccl00 = ==→o≡ ( record { eq→ = ? ; eq← = ? } )
72 91
73 -- Subbase P 92 -- Subbase P
74 -- A set of countable intersection of P will be a base (x ix an element of the base) 93 -- A set of countable intersection of P will be a base (x ix an element of the base)
75 94
76 data Subbase (P : HOD) : Ordinal → Set n where 95 data Subbase (P : HOD) : Ordinal → Set n where
484 (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp))) 503 (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)))
485 504
486 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP 505 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
487 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF 506 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
488 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where 507 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where
508 CF : HOD
509 CF = Replace' (filter F) (λ x fx → Cl TP x (λ {w} xw → LP (f⊆L F fx) _ (subst (λ k → odef k w) (sym *iso) xw )) )
510 CF⊆CS : CF ⊆ CS TP
511 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ subst (λ k → k ⊆ P) (trans (sym *iso) (sym (cong (*) x=ψz))) uf01 , uf02 ⟫ where
512 uf01 : (Cl TP (* z) (λ {w} xw → LP (f⊆L F (subst (odef (filter F)) (sym &iso) az)) w (subst (λ k → odef k w) (sym *iso) xw))) ⊆ P
513 uf01 = ?
514 uf02 : odef (OS TP) (& (P ＼ * x))
515 uf02 = ?
489 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v 516 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v
490 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ? 517 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?
491 518
492 -- product topology of compact topology is compact 519 -- product topology of compact topology is compact
493 520