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

comparison src/Topology.agda @ 1180:8e04e3cad0b5

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 Thu, 23 Feb 2023 18:44:47 +0900
parents f4cd937759fc
children cf25490dd112
comparison
equal deleted inserted replaced
1179:f4cd937759fc 1180:8e04e3cad0b5
444 & (L ＼ * y ) 444 & (L ＼ * y )
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 open _==_
450
449 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 451 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
450 Compact→FIP {L} top fip with trio< (& L) o∅ 452 Compact→FIP {L} top compact with trio< (& L) o∅
451 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 453 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
452 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 454 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? }
453 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where 455 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
454 -- set of coset of X 456 -- set of coset of X
455 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal 457 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
461 comp01 = subst (λ k → odef (* X) k) (sym &iso) az 463 comp01 = subst (λ k → odef (* X) k) (sym &iso) az
462 464
463 -- if all finite intersection of (OX X) contains something, 465 -- 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) 466 -- 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 467 -- it means there is a limit
466 --
467 Intersection : (X : Ordinal ) → o∅ o< X → HOD -- ∩ X
468 Intersection X 0<X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = osuc X ; <odmax = i00 } where
469 i01 : HOD
470 i01 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
471 i02 : odef (* X) (& i01)
472 i02 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
473 i00 : {x : Ordinal} → ({y : Ordinal} → odef (* X) y → odef (* y) x) → x o< osuc X
474 i00 {x} xy = begin
475 x ≡⟨ sym &iso ⟩
476 & (* x) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) i03) ⟩
477 & i01 <⟨ c<→o< i02 ⟩
478 & (* X) ≡⟨ &iso ⟩
479 X ∎ where
480 open o≤-Reasoning O
481 i03 : odef (* (& i01)) x
482 i03 = xy i02
483 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 468 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
484 → ¬ ( Intersection X ? =h= od∅ ) 469 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ )
485 has-intersection {X} CX fip i=0 = ? where 470 has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = cover1 ; P∋cover = ? ; isCover = ? } where
471 cover1 : {x : Ordinal} → odef L x → Ordinal
472 cover1 {x} Lx = ?
486 no-cover : ¬ ( (* (OX CX)) covers L ) 473 no-cover : ¬ ( (* (OX CX)) covers L )
487 no-cover = ? 474 no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?) ) where
475 fp01 : Ordinal
476 fp01 = Compact.finCover compact (OOX CX) cov
477 fp02 : Subbase ? ?
478 fp02 = ?
488 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 479 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
489 → Ordinal 480 → Ordinal
490 limit = ? 481 limit {X} CX fip with trio< X o∅
482 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
483 ... | tri≈ ¬a b ¬c = o∅
484 ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c))
491 fip00 : {X : Ordinal} (CX : * X ⊆ CS top) 485 fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
492 (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 486 (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
493 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) 487 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
494 fip00 = ? 488 fip00 {X} CX fip {x} Xx with trio< X o∅
489 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
490 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) )
491 ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c )
492 ... | ⟪ 0<m , intersect ⟫ = intersect Xx
495 493
496 494
497 open Filter 495 open Filter
498 496
499 -- Ultra Filter has limit point 497 -- Ultra Filter has limit point