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

comparison src/Topology.agda @ 1162:0a6040d914f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closure in Topology
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 21 Jan 2023 01:52:19 +0900
parents b45925515f77
children cd54ee498249
comparison
equal deleted inserted replaced
1161:b45925515f77 1162:0a6040d914f8
64 P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1 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 ⟫ 65 , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos ⟫
66 66
67 open Topology 67 open Topology
68 68
69 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD 69 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD
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 ) } 70 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) }
71 ; odmax = & L ; <odmax = odef∧< } 71 ; odmax = & L ; <odmax = odef∧< }
72 72
73 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L 73 ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L
74 ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic 74 ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic
75 → 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)))
76 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) 76 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
77 77
78 record NAO {L : HOD} (top : Topology L) (A : HOD) (A⊆L : A ⊆ L) (o : Ordinal) : Set n where 78 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A
79 field 79 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS) where
80 ox : odef (OS top) o 80 OCl : HOD
81 na : ¬ ( A ⊆ * o) 81 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< }
82 82 OCl⊆OS : OCl ⊆ OS top
83 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → (A⊆L : A ⊆ L) → CS top ∋ Cl top A A⊆L 83 OCl⊆OS ox = proj1 ox
84 CS∋Cl {L} top A A⊆L = ⟪ (λ {x} cx → proj1 ( subst (λ k → odef k x) *iso cx )) , ? ⟫ where 84 UOCl-is-OS : OS top ∋ Union OCl
85 NCl : HOD 85 UOCl-is-OS = o∪ top OCl⊆OS
86 NCl = record { od = record { def = λ x → NAO top A A⊆L x } ; odmax = & (OS top) ; <odmax = λ lt → odef< (NAO.ox lt) } 86 cc00 : (L ＼ Union OCl) =h= Cl top A
87 NCl⊆OS : NCl ⊆ OS top 87 cc00 = record { eq→ = cc01 ; eq← = cc03 } where
88 NCl⊆OS {x} ncl = NAO.ox ncl 88 cc01 : {x : Ordinal} → odef (L ＼ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x)
89 ccl00 : (L ＼ (Cl top A A⊆L)) ≡ Union NCl 89 cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where
90 ccl00 = ==→o≡ ( record { eq→ = ccl01 ; eq← = ? } ) where 90 cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x → odef (* c) x
91 ccl01 : {x : Ordinal} → odef (L ＼ Cl top A A⊆L) x → odef (Union NCl) x 91 cc02 c cc ac nox with ODC.∋-p O (* c) (* x)
92 ccl01 {x} ⟪ Lx , nclx ⟫ with ODC.∋-p O A (* x) 92 ... | yes y = subst (λ k → odef (* c) k) &iso y
93 ... | yes A∋x = ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ac (subst (λ k → odef A k) &iso A∋x) ) ⟫ ) 93 ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) (sym *iso) cc06 } ) where
94 ... | no ¬A∋x with ODC.p∨¬p O (NCl =h= od∅) 94 cc06 : odef (L ＼ * c) x
95 ... | case1 ¬nao = ? 95 cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫
96 ... | case2 nao = record { owner = & o ; ao = ODC.x∋minimal O NCl nao ; ox = subst (λ k → odef k x) (sym *iso) ccl02 } where 96 cc08 : * c ⊆ L
97 o = minimal NCl nao 97 cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc )
98 ccl02 : odef o x 98 cc07 : A ⊆ (L ＼ * (& (L ＼ * c)))
99 ccl02 with ODC.∋-p O o (* x) 99 cc07 {z} az = subst (λ k → odef k z ) (
100 ... | yes y = subst (λ k → odef o k) &iso y 100 begin * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩
101 ... | no ¬ox = ⊥-elim ( nclx ⟪ Lx , ? ⟫ ) 101 L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩
102 -- not A∋x, ¬ ( A ⊆ o) → A ⊆ (L ＼ o) → (L ＼ o) ∋ x 102 L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning
103 -- ¬ox → (L ＼ o) ∋ x, A ⊆ (L ＼ o) → 103 -- ksubst ( λ k → A ⊆ ( L ＼ k )) *iso (subst (λ k → A ⊆ k ) (L＼Lx=x ? ) (ac az) )
104 -- ⊥-elim ( NAO.na (ODC.x∋minimal O NCl nao) ( λ oa → ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ? ) ⟫ ))) 104 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x
105 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where
106 cc04 : ¬ odef (Union OCl) x
107 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where
108 cc05 : odef (* (& (L ＼ * o))) x
109 cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) (sym *iso) A⊆L-o)
105 110
106 111
107 -- Subbase P 112 -- Subbase P
108 -- A set of countable intersection of P will be a base (x ix an element of the base) 113 -- A set of countable intersection of P will be a base (x ix an element of the base)
109 114
517 ( MaximumFilter.mf (maxf CSX fp) ) 522 ( MaximumFilter.mf (maxf CSX fp) )
518 (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp))) 523 (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)))
519 524
520 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP 525 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
521 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF 526 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
522 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where 527 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
523 CF : HOD 528 CF : HOD
524 CF = Replace' (filter F) (λ x fx → Cl TP x (λ {w} xw → LP (f⊆L F fx) _ (subst (λ k → odef k w) (sym *iso) xw )) ) 529 CF = Replace' (filter F) (λ x fx → Cl TP x )
525 CF⊆CS : CF ⊆ CS TP 530 CF⊆CS : CF ⊆ CS TP
526 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 531 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z))
527 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 532 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
528 uf01 = ? 533 ufl01 = ?
529 uf02 : odef (OS TP) (& (P ＼ * x))
530 uf02 = ?
531 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v 534 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v
532 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ? 535 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?
533 536
534 -- product topology of compact topology is compact 537 -- product topology of compact topology is compact
535 538