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

comparison src/Topology.agda @ 1175:7d2bae0ff36b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Feb 2023 12:02:41 +0900
parents f4bccbe80540
children ae586d6275c2
comparison
equal deleted inserted replaced
1174:375615f9d60f 1175:7d2bae0ff36b
445 ∎ where open ≡-Reasoning 445 ∎ where open ≡-Reasoning
446 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w 446 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
447 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw 447 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
448 448
449 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 449 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
450 Compact→FIP = ? 450 Compact→FIP {L} top fip with trio< (& L) o∅
451 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
452 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? }
453 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
454 -- set of coset of X
455 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
456 OX {X} ox = & ( Replace' (* X) (λ z xz → L ＼ z ))
457 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top
458 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
459 ... | 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
460 comp01 : odef (* X) (& (* z))
461 comp01 = subst (λ k → odef (* X) k) (sym &iso) az
462 --
463 -- if all finite intersection of (OX X) contains something,
464 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
465 -- it means there is a limit
466 --
467 Intersection : (X : Ordinal ) → HOD
468 Intersection X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = ? ; <odmax = ? }
469 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
470 → ¬ ( Intersection X =h= od∅ )
471 has-intersection {X} CX fip i=0 = ? where
472 no-cover : ¬ ( (* (OX CX)) covers L )
473 no-cover = ?
474 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
475 → Ordinal
476 limit = ?
477 fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
478 (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
479 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
480 fip00 = ?
481
451 482
452 open Filter 483 open Filter
453 484
454 -- Ultra Filter has limit point 485 -- Ultra Filter has limit point
455 486