Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1178:7bd348551d37
fix
author | Shinji Kono |
---|---|
date | Thu, 23 Feb 2023 09:58:11 +0800 |
parents | 66355bace86f |
children | f4cd937759fc |
files | src/Topology.agda src/VL.agda |
diffstat | 2 files changed, 12 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Wed Feb 22 12:01:09 2023 +0900 +++ b/src/Topology.agda Thu Feb 23 09:58:11 2023 +0800 @@ -279,12 +279,19 @@ fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal -fipx {L} top {X} X⊆CS fip with fip (λ x → x) (gi ?) -... | t = ? +fipx {L} top {X} X⊆CS fip with trio< X o∅ +... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) +... | tri≈ ¬a b ¬c = o∅ +... | tri> ¬a ¬b c = & (ODC.minimal O (* fip00) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) ( fip (λ x → x ) (gi ? ) )))) where + fip00 : ? + fip00 = & (ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) c ) )) fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top ) → (fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → odef (* X) (fipx top X⊆CS fip) -fipX∋x = ? +fipX∋x {L} top {X} X⊆CS fip with trio< X o∅ +... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) +... | tri≈ ¬a b ¬c = ? +... | tri> ¬a ¬b c = ? -- fip (λ x → x) (gi ?) -- Compact @@ -468,7 +475,7 @@ ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P\CS=OS top (cs comp01)) where comp01 : odef (* X) (& (* z)) comp01 = subst (λ k → odef (* X) k) (sym &iso) az - -- + -- if all finite intersection of (OX 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