Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1226:c8f5376a9623
proj2 filter F done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Mar 2023 18:58:23 +0900 |
| parents | 5c4a088ae95b |
| children | 72b5815be243 |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 28 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Tue Mar 07 18:24:42 2023 +0900 +++ b/src/Tychonoff.agda Tue Mar 07 18:58:23 2023 +0900 @@ -484,7 +484,8 @@ ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p)) ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} - (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ? + (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) + (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp ) ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp )) uflp : UFLP TP FP UFP @@ -514,7 +515,7 @@ b=x : b ≡ x b=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x - ty22 {x} qx = record { z = _ ; az = ab-pair ? ? ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where + ty22 {x} qx = record { z = _ ; az = ab-pair qq qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where ty12 : * x ≡ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ty12 = begin * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩ @@ -538,7 +539,7 @@ Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ≡⟨ Replace'-iso _ ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ⟩ Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ - fx→qx fq ≡⟨ fx→qx1 ? fq ⟩ + fx→qx fq ≡⟨ fx→qx1 ap fq ⟩ q ∎ where open ≡-Reasoning FQSet⊆PP : FQSet ⊆ Power Q FQSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw @@ -567,23 +568,23 @@ ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) - q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ P + q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ Q q⊆Q {x} {p} fx x=ψz {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw - ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) - ? -- (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) + (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) FQ : Filter {Power Q} {Q} (λ x → x) FQ = record { filter = FQSet ; f⊆L = FQSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where ty01 : {p q : HOD} → Power Q ∋ q → FQSet ∋ p → p ⊆ q → FQSet ∋ q - ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq ? ? -- q⊆P (ty10 ty05 ty06 ) + ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq q⊆P (ty10 ty05 ty06 ) where - -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy)) - -- x = ( qx , qx ) , qx ⊆ q + -- p ≡ (Replace' (* x) (λ y xy → (zπ2 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy)) + -- x = ( px , qx ) , qx ⊆ q ty03 : Power (ZFP P Q) ∋ ZFP P q - ty03 z zpq = isQ→PxQ {* (& q)} ? ? -- ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) (Pq _) + ty03 z zpq = isQ→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) q⊆P : q ⊆ Q q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) ty05 : filter F ∋ ZFP P p - ty05 = filter1 F (λ z wz → isQ→PxQ ? ? ) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆qxq fx x=ψz) + ty05 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆qxq fx x=ψz) ty06 : ZFP P p ⊆ ZFP P q ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q @@ -591,27 +592,27 @@ ty02 : {p q : HOD} → FQSet ∋ p → FQSet ∋ q → Power Q ∋ (p ∩ q) → FQSet ∋ (p ∩ q) ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq - = FQSet∋zpq ? ? where -- (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where - ty54 : Power (ZFP P Q) ∋ (ZFP P q ∩ ZFP P q ) + = FQSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where + ty54 : Power (ZFP P Q) ∋ (ZFP P p ∩ ZFP P q ) ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where pqz : odef (ZFP P (p ∩ q) ) z - pqz = ? -- subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz + pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz pqz1 : odef P (zπ1 pqz) pqz1 = zp1 pqz pqz2 : odef Q (zπ2 pqz) - pqz2 = ? -- q⊆Q fzp x=ψzp (proj2 (zp2 pqz)) - ty53 : filter F ∋ ZFP P q - ty53 = ? -- filter1 F (λ z wz → isQ→PxQ ? -- (q⊆Q fzp x=ψzp) - -- (subst (λ k → odef k z) *iso wz)) - -- (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp) + pqz2 = q⊆Q fzp x=ψzp (proj1 (zp2 pqz)) + ty53 : filter F ∋ ZFP P p + ty53 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzp x=ψzp) + (subst (λ k → odef k z) *iso wz)) + (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp) ty52 : filter F ∋ ZFP P q - ty52 = ? -- filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) - -- (subst (λ k → odef k z) *iso wz)) - -- (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq) - ty51 : filter F ∋ ( ZFP P q ∩ ZFP q Q ) - ty51 = ? -- filter2 F ty53 ty52 ty54 + ty52 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) + (subst (λ k → odef k z) *iso wz)) + (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq) + ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q ) + ty51 = filter2 F ty53 ty52 ty54 ty50 : filter F ∋ ZFP P (p ∩ q) - ty50 = ? -- subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 + ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51 UFQ : ultra-filter FQ UFQ = record { proper = ty61 ; ultra = ty60 } where ty61 : ¬ (FQSet ∋ od∅) @@ -623,7 +624,8 @@ ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az ty60 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (FQSet ∋ p) ∨ (FQSet ∋ (Q ＼ p)) ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q} - (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ? + (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) + (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) ... | case1 fq = case1 (FQSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fq ) ... | case2 fnp = case2 (FQSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj2 ZFP\Q)) fnp ))