Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1214:93e1869bb57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Mar 2023 13:41:57 +0900
parents 22de2d4f7271
children 881e85e12e38
files src/Tychonoff.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Sun Mar 05 12:16:07 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 13:41:57 2023 +0900
@@ -359,7 +359,13 @@
                   ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
                        (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 ))  )
                   x⊆pxq : * x ⊆ ZFP p Q
-                  x⊆pxq = ?
+                  x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
+                  ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
+                      ty07 : odef (* x) (& < * a , * b >) 
+                      ty07 = xw
+                      ty08 : odef p a
+                      ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))  
+                           record { z = _ ; az = xw ;  x=ψz = ? }
                   ty05 : filter F ∋  ZFP p Q
                   ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq
                   ty06 : ZFP p Q ⊆ ZFP q Q