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

comparison src/ODUtil.agda @ 1483:2435deeecda9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
maxfilter fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 30 Jun 2024 19:36:51 +0900
parents 6752e2ff4dc6
children 5dacb669f13b
comparison
equal deleted inserted replaced
1482:4f597bc6b3d6 1483:2435deeecda9
47 ⊆∩-incl-1 : {a b c : HOD} → a ⊆ c → ( a ∩ b ) ⊆ c 47 ⊆∩-incl-1 : {a b c : HOD} → a ⊆ c → ( a ∩ b ) ⊆ c
48 ⊆∩-incl-1 {a} {b} {c} a<c {z} ab = a<c (proj1 ab) 48 ⊆∩-incl-1 {a} {b} {c} a<c {z} ab = a<c (proj1 ab)
49 49
50 ⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c 50 ⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c
51 ⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab) 51 ⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab)
52
53 *iso∩ : {p q : HOD} → (p ∩ q) =h= (* (& p) ∩ * (& q))
54 eq→ (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq← *iso px , eq← *iso qx ⟫
55 eq← (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq→ *iso px , eq→ *iso qx ⟫
52 56
53 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A 57 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
54 power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where 58 power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where
55 t1 : {x : HOD } → t ∋ x → A ∋ x 59 t1 : {x : HOD } → t ∋ x → A ∋ x
56 t1 = power→ A t PA∋t 60 t1 = power→ A t PA∋t