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

comparison src/Topology.agda @ 1118:441ad880a45d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Product Topology done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Jan 2023 20:28:07 +0900
parents 53ca3c609f0e
children 5b0525cb9a5d
comparison
equal deleted inserted replaced
1117:53ca3c609f0e 1118:441ad880a45d
193 193
194 base : {P Q : HOD} → Topology P → Topology Q → HOD 194 base : {P Q : HOD} → Topology P → Topology Q → HOD
195 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? } 195 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
196 196
197 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) 197 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
198 _Top⊗_ {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (base TP TQ) ? 198 _Top⊗_ {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (base TP TQ) record { P⊆PL = tp00 } where
199 tp00 : base TP TQ ⊆ Power (ZFP P Q)
200 tp00 {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where
201 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
202 tp01 w wz with subst (λ k → odef k w ) *iso wz
203 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
204 tp03 : odef P a
205 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
206 tp00 {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where
207 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
208 tp01 w wz with subst (λ k → odef k w ) *iso wz
209 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where
210 tp03 : odef Q b
211 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
199 212
200 -- existence of Ultra Filter 213 -- existence of Ultra Filter
201 214
202 open Filter 215 open Filter
203 216