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

comparison src/Tychonoff.agda @ 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
comparison
equal deleted inserted replaced
1213:22de2d4f7271 1214:93e1869bb57c
357 p⊆P : p ⊆ P 357 p⊆P : p ⊆ P
358 p⊆P {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw 358 p⊆P {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw
359 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 359 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso))
360 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) 360 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) )
361 x⊆pxq : * x ⊆ ZFP p Q 361 x⊆pxq : * x ⊆ ZFP p Q
362 x⊆pxq = ? 362 x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
363 ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
364 ty07 : odef (* x) (& < * a , * b >)
365 ty07 = xw
366 ty08 : odef p a
367 ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))
368 record { z = _ ; az = xw ; x=ψz = ? }
363 ty05 : filter F ∋ ZFP p Q 369 ty05 : filter F ∋ ZFP p Q
364 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 370 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
365 ty06 : ZFP p Q ⊆ ZFP q Q 371 ty06 : ZFP p Q ⊆ ZFP q Q
366 ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq 372 ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
367 ty02 : filter F ∋ ZFP q Q 373 ty02 : filter F ∋ ZFP q Q