Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1221:0e8306b146f6
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 06 Mar 2023 20:13:00 +0900 |
| parents | a8253c91f630 |
| children | 9f955d49e162 |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 11 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Mon Mar 06 15:23:17 2023 +0900 +++ b/src/Tychonoff.agda Mon Mar 06 20:13:00 2023 +0900 @@ -451,13 +451,13 @@ x⊆pxq : * ? ⊆ ZFP p Q x⊆pxq = ? ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q) - ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso ty55) (ab-pair ty551 ty552 ) where - ty55 : odef (ZFP (p ∩ q) Q) z - ty55 = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz - ty551 : odef P (zπ1 ty55) - ty551 = ? - ty552 : odef Q (zπ2 ty55) - ty552 = ? + ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where + pqz : odef (ZFP (p ∩ q) Q) z + pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz + pqz1 : odef P (zπ1 pqz) + pqz1 = ? + pqz2 : odef Q (zπ2 pqz) + pqz2 = ? ty53 : filter F ∋ ZFP p Q ty53 = filter1 F (λ z wz → isP→PxQ ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq ty52 : filter F ∋ ZFP q Q @@ -494,6 +494,10 @@ pqb⊆opq = Base.b⊆u bpq base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → * b ⊆ filter F base⊆F (gi (case1 px)) b⊆u {z} bz = fz where + -- F is ultra, so F ∋ b ∨ F ∋ (ZFP P Q ＼ b) + -- FP ∋ b ∨ FQ ∋ b + -- Neighbor b ∋ limit + -- F ∋ (ZFP P Q ＼ b) → ¬ Neighbor b ∋ limit → ⊥ -- F contains no od∅, because it projection contains no od∅ -- x is an element of BaseP, which is a subset of Neighbor npq -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)