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

changeset 1295:503ec16e5c28

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 Fri, 02 Jun 2023 12:04:43 +0900
parents 968feed7cf64
children 428227847d62
files src/ZProduct.agda
diffstat 1 files changed, 6 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/ZProduct.agda	Fri Jun 02 08:52:13 2023 +0900
+++ b/src/ZProduct.agda	Fri Jun 02 12:04:43 2023 +0900
@@ -372,6 +372,12 @@
             lemma1 : & < * b , * a > o< osuc (& (Power (Union (B , A))))
             lemma1 = ⊆→o≤ (ZFP<AB (subst (λ k → odef B k) (sym &iso) bb) (subst (λ k → odef A k) (sym &iso) aa)  )
 
+ZPmirror⊆ZFPBA : (A B C : HOD) → (cab : C  ⊆ ZFP A B ) → ZPmirror A B C cab ⊆ ZFP B A
+ZPmirror⊆ZFPBA A B C cab {z} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } 
+    = subst (λ k → odef (ZFP B A) k) (sym x=ba) lemma2 where
+        lemma2 : odef (ZFP B A) (& < * b , * a > )
+        lemma2 = ZFP→ (subst (λ k → odef B k ) (sym &iso) bb) (subst (λ k → odef A k ) (sym &iso) aa) 
+
 ZPmirror-iso : (A B C : HOD)  → (cab : C  ⊆ ZFP A B ) → ( {x y : HOD} → C ∋ < x , y > →  ZPmirror A B C cab ∋ < y , x > ) 
                                                        ∧ ( {x y : HOD} →  ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y > )
 ZPmirror-iso A B C cab = ⟪ zs00 refl   , zs01 ⟫ where