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

changeset 1181:cf25490dd112

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 24 Feb 2023 11:52:44 +0800
parents 8e04e3cad0b5
children 0727cf865ebd
files src/Topology.agda
diffstat 1 files changed, 9 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Thu Feb 23 18:44:47 2023 +0900
+++ b/src/Topology.agda	Fri Feb 24 11:52:44 2023 +0800
@@ -467,9 +467,15 @@
    --     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 = cover1 ; P∋cover = ? ; isCover = ? } where
-       cover1 :  {x : Ordinal} → odef L x → Ordinal
-       cover1 {x} Lx = ?
+   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 : Ordinal} → odef (* X) y → Ordinal
+          fp04 {y} xy = & (L ＼ * y)
+          fp03 : ?
+          fp03 = ?
        no-cover : ¬ ( (* (OX CX)) covers L ) 
        no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?)  ) where
           fp01 : Ordinal