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

changeset 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
files src/Topology.agda
diffstat 1 files changed, 14 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 01 20:07:04 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 20:28:07 2023 +0900
@@ -195,7 +195,20 @@
 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
 
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) ?
+_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) record { P⊆PL = tp00 } where
+    tp00 : base TP TQ ⊆ Power (ZFP P Q)
+    tp00 {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+        tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
+        tp01 w wz with subst (λ k → odef k w ) *iso wz
+        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
+            tp03 : odef P a
+            tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
+    tp00 {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+        tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
+        tp01 w wz with subst (λ k → odef k w ) *iso wz
+        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
+            tp03 : odef Q b
+            tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
 
 -- existence of Ultra Filter