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

comparison src/Topology.agda @ 1182:0727cf865ebd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 24 Feb 2023 15:00:23 +0800
parents cf25490dd112
children f5deac708524
comparison
equal deleted inserted replaced
1181:cf25490dd112 1182:0727cf865ebd
470 has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = ? ; P∋cover = ? ; isCover = ? } where 470 has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = ? ; P∋cover = ? ; isCover = ? } where
471 cover1 : {x : Ordinal} → odef L x → Own (* (OX CX)) x 471 cover1 : {x : Ordinal} → odef L x → Own (* (OX CX)) x
472 cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x) 472 cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x)
473 ... | case1 p = p 473 ... | case1 p = p
474 ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where 474 ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where
475 fp04 : {y : Ordinal} → odef (* X) y → Ordinal 475 fp04 : {y x : Ordinal} → odef (* X) y → ¬ odef (L ＼ * y) x
476 fp04 {y} xy = & (L ＼ * y) 476 fp04 {y} {x} xy ⟪ Lx , nx ⟫ = ?
477 fp03 : ? 477 fp03 : ?
478 fp03 = ? 478 fp03 = ?
479 no-cover : ¬ ( (* (OX CX)) covers L ) 479 no-cover : ¬ ( (* (OX CX)) covers L )
480 no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?) ) where 480 no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?) ) where
481 fp01 : Ordinal 481 fp01 : Ordinal