Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1183:f5deac708524
...
author | kono |
---|---|
date | Sat, 25 Feb 2023 11:24:45 +0800 (2023-02-25) |
parents | 0727cf865ebd |
children | 0b2d03711aff |
files | src/Topology.agda |
diffstat | 1 files changed, 14 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Fri Feb 24 15:00:23 2023 +0800 +++ b/src/Topology.agda Sat Feb 25 11:24:45 2023 +0800 @@ -462,26 +462,28 @@ comp01 : odef (* X) (& (* z)) comp01 = subst (λ k → odef (* X) k) (sym &iso) az - -- if all finite intersection of (OX X) contains something, + -- if all finite intersection of X contains something, -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) -- it means there is a limit has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) - has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = ? ; P∋cover = ? ; isCover = ? } where - cover1 : {x : Ordinal} → odef L x → Own (* (OX CX)) x - cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x) - ... | case1 p = p - ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where - fp04 : {y x : Ordinal} → odef (* X) y → ¬ odef (L \ * y) x - fp04 {y} {x} xy ⟪ Lx , nx ⟫ = ? - fp03 : ? - fp03 = ? - no-cover : ¬ ( (* (OX CX)) covers L ) - no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?) ) where + has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , fp05 ⟫ )) where + no-cover : ¬ ( (* (OX CX)) covers L ) + no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?) ) where fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov fp02 : Subbase ? ? fp02 = ? + record NC : Set n where + field + nc : Ordinal + is-nc : {y : Ordinal} → odef (* (OX CX)) y → ¬ (odef (* y) nc ) + fp03 : NC + fp03 with ODC.p∨¬p O NC + ... | case1 nc = nc + ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → ? ; P∋cover = ? ; isCover = ? } ) + fp05 : {y : Ordinal } → odef (* X) y → odef ( * y) ? + fp05 = ? limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) → Ordinal limit {X} CX fip with trio< X o∅