Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1146:1966127fc14f
wrong cover definition
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 16 Jan 2023 10:50:30 +0900 |
| parents | f8c3537e68a6 |
| children | 607a79aef297 d39c79bb71f0 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 10 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Mon Jan 16 02:22:03 2023 +0900 +++ b/src/Topology.agda Mon Jan 16 10:50:30 2023 +0900 @@ -241,7 +241,16 @@ -- FIP is Compact FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top -FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where +FIP→Compact {L} top fip with trio< (& L) o∅ +... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) +... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → & ( od∅ , od∅ ) ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where + fip02 : {x : Ordinal } → ¬ odef L x + fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) ) + fip01 : {X : Ordinal } → (xcp : * X covers L) → * (& ( od∅ , od∅ )) covers L + fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } + fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (& ( od∅ , od∅ )) + fip00 {X} xo xcp = fin-e ? +... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where -- set of coset of X CX : {X : Ordinal} → * X ⊆ OS top → Ordinal CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼ z ))