Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1194:6174001ba1c0
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Feb 2023 15:01:17 +0900 |
| parents | e110b56d8cbe |
| children | 68239d102d15 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 54 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Mon Feb 27 07:29:11 2023 +0800 +++ b/src/Topology.agda Tue Feb 28 15:01:17 2023 +0900 @@ -389,7 +389,13 @@ fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers - (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where + (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where + fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c + fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) + ; isCover = isCover cov } + fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c + fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) + ; isCover = isCover cov } fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b)) fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ @@ -424,7 +430,6 @@ ... | 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 comp01 : odef (* X) (& (* z)) comp01 = subst (λ k → odef (* X) k) (sym &iso) az - -- if all finite intersection of X contains something, -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) -- it means there is a limit @@ -436,17 +441,40 @@ 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 ( SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov) ) fp12 ) where fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov - fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) ) - fp02 t fin-e = gi ? - fp02 t (fin-i tx ) = gi fp03 where - fp03 : odef (* X) (& (L ＼ * t)) - fp03 = ? - fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x) (fp02 ty y ) ) where - fp04 : & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) - fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where + record SB (t : Ordinal) : Set n where + field + i : Ordinal + ¬i⊆Ut : ¬ ( (L ＼ * i) ⊆ Union (* t)) + sb : Subbase (* X) (& (L ＼ * i)) + fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t + fp02 t fin-e = record { i = & ( L ＼ fp07) ; ¬i⊆Ut = fp20 ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) } 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))) + fp20 : ¬ (L ＼ * (& (L ＼ fp07))) ⊆ Union (* o∅) + fp20 lt = ? + fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; ¬i⊆Ut = fp23 } where + fp23 : ¬ (L ＼ * x) ⊆ Union (* (& (* x , * x))) + fp23 = ? + 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 + fip34 : * z1 ⊆ L + fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 + fip33 : z1 ≡ & (L ＼ * x) + fip33 = begin + z1 ≡⟨ sym &iso ⟩ + & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩ + & (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 ; ¬i⊆Ut = ? } 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 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where @@ -457,7 +485,21 @@ fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ - + fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))))) + fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx x)) (SB.sb (fp02 ty y )) ) + fp12 : (L ＼ * (SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)))) ⊆ Union (* fp01) + fp12 {x} ⟪ Lx , not ⟫ = ⊥-elim ( fp14 (λ {y} lt → record { owner = cover fcov (fp16 lt) + ; ao = P∋cover fcov (fp16 lt) + ; ox = isCover fcov (fp16 lt) } )) where + fcov = Compact.isCover compact (OOX CX) cov + fp13 : Ordinal + fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)) + fp16 : {y : Ordinal} → odef (L ＼ * fp13) y → odef L y + fp16 {y} ⟪ Ly , _ ⟫ = Ly + fp15 : ¬ ( odef (* fp13) x) + fp15 = not + fp14 : ¬ ( (L ＼ * fp13 ) ⊆ Union (* fp01 )) + fp14 = SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)) record NC : Set n where -- x is not covered field x : Ordinal