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

changeset 1183:f5deac708524

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Sat, 25 Feb 2023 11:24:45 +0800
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∅