Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1162:0a6040d914f8
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 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 41 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Fri Jan 20 22:33:30 2023 +0900 +++ b/src/Topology.agda Sat Jan 21 01:52:19 2023 +0900 @@ -66,42 +66,47 @@ open Topology -Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD -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 ) } +Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD +Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } ; odmax = & L ; <odmax = odef∧< } -ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L -ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic +ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L +ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) -record NAO {L : HOD} (top : Topology L) (A : HOD) (A⊆L : A ⊆ L) (o : Ordinal) : Set n where - field - ox : odef (OS top) o - na : ¬ ( A ⊆ * o) - -CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → (A⊆L : A ⊆ L) → CS top ∋ Cl top A A⊆L -CS∋Cl {L} top A A⊆L = ⟪ (λ {x} cx → proj1 ( subst (λ k → odef k x) *iso cx )) , ? ⟫ where - NCl : HOD - NCl = record { od = record { def = λ x → NAO top A A⊆L x } ; odmax = & (OS top) ; <odmax = λ lt → odef< (NAO.ox lt) } - NCl⊆OS : NCl ⊆ OS top - NCl⊆OS {x} ncl = NAO.ox ncl - ccl00 : (L ＼ (Cl top A A⊆L)) ≡ Union NCl - ccl00 = ==→o≡ ( record { eq→ = ccl01 ; eq← = ? } ) where - ccl01 : {x : Ordinal} → odef (L ＼ Cl top A A⊆L) x → odef (Union NCl) x - ccl01 {x} ⟪ Lx , nclx ⟫ with ODC.∋-p O A (* x) - ... | yes A∋x = ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ac (subst (λ k → odef A k) &iso A∋x) ) ⟫ ) - ... | no ¬A∋x with ODC.p∨¬p O (NCl =h= od∅) - ... | case1 ¬nao = ? - ... | case2 nao = record { owner = & o ; ao = ODC.x∋minimal O NCl nao ; ox = subst (λ k → odef k x) (sym *iso) ccl02 } where - o = minimal NCl nao - ccl02 : odef o x - ccl02 with ODC.∋-p O o (* x) - ... | yes y = subst (λ k → odef o k) &iso y - ... | no ¬ox = ⊥-elim ( nclx ⟪ Lx , ? ⟫ ) - -- not A∋x, ¬ ( A ⊆ o) → A ⊆ (L ＼ o) → (L ＼ o) ∋ x - -- ¬ox → (L ＼ o) ∋ x, A ⊆ (L ＼ o) → - -- ⊥-elim ( NAO.na (ODC.x∋minimal O NCl nao) ( λ oa → ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ? ) ⟫ ))) +CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A +CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS) where + OCl : HOD + OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< } + OCl⊆OS : OCl ⊆ OS top + OCl⊆OS ox = proj1 ox + UOCl-is-OS : OS top ∋ Union OCl + UOCl-is-OS = o∪ top OCl⊆OS + cc00 : (L ＼ Union OCl) =h= Cl top A + cc00 = record { eq→ = cc01 ; eq← = cc03 } where + cc01 : {x : Ordinal} → odef (L ＼ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) + cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where + cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x → odef (* c) x + cc02 c cc ac nox with ODC.∋-p O (* c) (* x) + ... | yes y = subst (λ k → odef (* c) k) &iso y + ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) (sym *iso) cc06 } ) where + cc06 : odef (L ＼ * c) x + cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫ + cc08 : * c ⊆ L + cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc ) + cc07 : A ⊆ (L ＼ * (& (L ＼ * c))) + cc07 {z} az = subst (λ k → odef k z ) ( + begin * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩ + L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩ + L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning + -- ksubst ( λ k → A ⊆ ( L ＼ k )) *iso (subst (λ k → A ⊆ k ) (L＼Lx=x ? ) (ac az) ) + cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x + cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where + cc04 : ¬ odef (Union OCl) x + cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where + cc05 : odef (* (& (L ＼ * o))) x + 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) -- Subbase P @@ -519,15 +524,13 @@ FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF -FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where +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 CF : HOD - CF = Replace' (filter F) (λ x fx → Cl TP x (λ {w} xw → LP (f⊆L F fx) _ (subst (λ k → odef k w) (sym *iso) xw )) ) + CF = Replace' (filter F) (λ x fx → Cl TP x ) CF⊆CS : CF ⊆ CS TP - 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 - 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 - uf01 = ? - uf02 : odef (OS TP) (& (P ＼ * x)) - uf02 = ? + 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)) + ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x + ufl01 = ? ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?