Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Topology.agda @ 1180:8e04e3cad0b5
...
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 |