Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1196:e7c3bd9e7c3e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Feb 2023 22:33:13 +0900 |
| parents | 68239d102d15 |
| children | 0a88fcd5d1c9 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 22 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Tue Feb 28 19:05:58 2023 +0900 +++ b/src/Topology.agda Tue Feb 28 22:33:13 2023 +0900 @@ -441,20 +441,21 @@ fp08 : odef (* X) (& fp07) fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) no-cover : ¬ ( (* (OX CX)) covers L ) - no-cover cov = ⊥-elim ? where + no-cover cov = ⊥-elim (f20 (Compact.isCover compact (OOX CX) cov)) where fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov record SB (t : Ordinal) : Set n where field i : Ordinal sb : Subbase (* X) (& (L ＼ * i)) + not-t : (L ＼ * i) ⊆ (L ＼ Union ( * t ) ) fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t - fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) } where + fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = ? } where fp22 : fp07 ⊆ L fp22 {x} lt = cs⊆L top (CX fp08) lt fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07))) fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso))) - fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 } where + fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = ? } where fp03 : odef (* X) (& (L ＼ * x)) fp03 with subst (λ k → odef k x ) *iso tx ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where @@ -467,7 +468,7 @@ & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ & (L ＼ * x ) ∎ where open ≡-Reasoning - fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 } where + fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = ? } where fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x @@ -499,10 +500,23 @@ fp17 {y} lt = record { owner = cover fcov (fp16 lt) ; ao = P∋cover fcov (fp16 lt) ; ox = isCover fcov (fp16 lt) } fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov) fcov = Compact.isFinite compact (OOX CX) cov - ¬i⊆Ut : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → ¬ ( (L ＼ * i) =h= od∅ ) - ¬i⊆Ut {i} sb = 0<P→ne (fip sb) - f20 : (cov : (* (OX CX)) covers L ) → ¬ ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) - f20 = ? + 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i) + 0<sb {i} sb = fip sb + sb : SB (Compact.finCover compact (OOX CX) cov) + sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) + f20 : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) + f20 fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where + f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) + f23 = SB.not-t sb + f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ + f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where + f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x ) + f24 {x} ⟪ Lx , not ⟫ = not record { owner = cover fcovers Lx ; ao = P∋cover fcovers Lx ; ox = isCover fcovers Lx } + f25 : & od∅ o< (& (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ) + f25 = ordtrans<-≤ (subst (λ k → k o< & (L ＼ * (SB.i sb))) (sym ord-od∅) (0<sb (SB.sb sb) ) ) ( begin + & (L ＼ * (SB.i sb)) ≤⟨ ⊆→o≤ f23 ⟩ + & (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ∎ ) where open o≤-Reasoning O + record NC : Set n where -- x is not covered field x : Ordinal