Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1197:0a88fcd5d1c9
... almost
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 01 Mar 2023 00:37:34 +0900 |
| parents | e7c3bd9e7c3e |
| children | 6e0cc71097e0 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 45 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Tue Feb 28 22:33:13 2023 +0900 +++ b/src/Topology.agda Wed Mar 01 00:37:34 2023 +0900 @@ -420,7 +420,11 @@ Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top Compact→FIP {L} top compact with trio< (& L) o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) -... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } +... | tri≈ ¬a b ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX xx) } where + fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ¬ odef (* X) x + fip000 {X} {x} CX xx = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) b)) o∅≡od∅ ) (sym &iso) + ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) ? )) + -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) )) ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where -- set of coset of X OX : {X : Ordinal} → * X ⊆ CS top → Ordinal @@ -450,12 +454,19 @@ 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) ; not-t = ? } where + fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = fp23 } 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 ; not-t = ? } where + fp23 : (L ＼ * (& (L ＼ fp07))) ⊆ (L ＼ Union (* o∅)) + fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫ + fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = fp24 } where + fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x)))) + fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25 ⟫ where + fp25 : ¬ odef (Union (* x , * x)) y + fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) + fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) 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 @@ -468,7 +479,37 @@ & (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 ; not-t = ? } where + fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = fp35 } where + fp35 : (L ＼ * (& (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty)))) + fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36 where + fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z + fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) ao )) + fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) *iso uz) where + fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z + fp41 x record { owner = .(& (* w)) ; ao = (case1 refl) ; ox = ox } = + os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox ) + fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } = + os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox ) + fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz + ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } + ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } + fp36 : (L ＼ (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* tx ∪ * ty)) + fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where + fp37 : ¬ odef (Union (* tx ∪ * ty)) z + fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where + fp38 : (L ＼ (* (SB.i (fp02 tx x)))) ⊆ (L ＼ Union (* tx)) + fp38 = SB.not-t (fp02 tx x) + fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx x))) + fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx x))} (fp40 x txw) + ... | case1 sb = sb + ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) + fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where + fp38 : (L ＼ (* (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* ty)) + fp38 = SB.not-t (fp02 ty y) + fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty y))) + fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty y))} (fp40 y tyw) + ... | case1 sb = sb + ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) 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