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

changeset 1112:fc3eea0d895d

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 Sat, 31 Dec 2022 22:09:31 +0900
parents b77a7f724663
children 384ba5a3c019
files src/Topology.agda
diffstat 1 files changed, 2 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sat Dec 31 22:04:23 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 22:09:31 2022 +0900
@@ -87,6 +87,8 @@
        tp01 {q} qp = ε-induction0 { λ x → x ⊆ Subbases P → Subbases P ∋ Union x } tp02 q qp where
            tp02 : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ Subbases P → Subbases P ∋ Union y) → x ⊆ Subbases P → Subbases P ∋ Union x
            tp02 {x} prev xp = gi ?
+       tp04 : {p q : HOD} → Subbases P ∋ p → Subbases P ∋ q → Subbases P ∋ (p ∩ q)
+       tp04 {p} {q} pp pq = subst (λ k → odef (Subbases P) k ) (cong₂ (λ j k → & ( j  ∩ k )) *iso *iso )  ( g∩ pp pq ) 
 
 
 -- covers