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

comparison src/Topology.agda @ 1184:0b2d03711aff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
....
author kono
date Sat, 25 Feb 2023 15:32:50 +0800
parents f5deac708524
children 807a55d55086
comparison
equal deleted inserted replaced
1183:f5deac708524 1184:0b2d03711aff
474 fp01 = Compact.finCover compact (OOX CX) cov 474 fp01 = Compact.finCover compact (OOX CX) cov
475 fp02 : Subbase ? ? 475 fp02 : Subbase ? ?
476 fp02 = ? 476 fp02 = ?
477 record NC : Set n where 477 record NC : Set n where
478 field 478 field
479 nc : Ordinal 479 x y : Ordinal
480 is-nc : {y : Ordinal} → odef (* (OX CX)) y → ¬ (odef (* y) nc ) 480 Lx : odef L x
481 fp03 : NC 481 Xy : odef (* X) y
482 fp03 with ODC.p∨¬p O NC 482 yx : odef (* y) x
483 ... | case1 nc = nc 483 fp03 : NC
484 ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → ? ; P∋cover = ? ; isCover = ? } ) 484 fp03 with ODC.p∨¬p O NC
485 fp05 : {y : Ordinal } → odef (* X) y → odef ( * y) ? 485 ... | case1 nc = nc
486 fp05 = ? 486 ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → ? ; P∋cover = ? ; isCover = ? } ) where
487 fp14 : {x : Ordinal} → odef L x → {y : Ordinal} → odef (* X) y → ¬ odef (* y) x
488 fp14 {x} Lx {y} Xy yx = ¬nc record { x = x ; Lx = Lx ; y = y ; Xy = Xy ; yx = yx }
489 fp06 : {x : Ordinal} → odef L x → HOD
490 fp06 {x} Lx = record { od = record { def = λ y → odef (* X) y → odef (L ＼ * y) x } ; odmax = ? ; <odmax = ? }
491 fp07 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( fp06 Lx =h= od∅ )
492 fp07 {x} Lx eq = ⊥-elim (¬x<0 {x} (eq→ eq fp08)) where
493 fp08 : {y : Ordinal} → odef (* X) y → odef (L ＼ * y) x
494 fp08 = ?
495 fp05 : {y : Ordinal } → odef (* X) y → odef ( * y) (NC.x fp03)
496 fp05 {y} Xy = ?
487 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 497 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
488 → Ordinal 498 → Ordinal
489 limit {X} CX fip with trio< X o∅ 499 limit {X} CX fip with trio< X o∅
490 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 500 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
491 ... | tri≈ ¬a b ¬c = o∅ 501 ... | tri≈ ¬a b ¬c = o∅