Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 269:30e419a2be24
disjunction and conjunction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 06 Oct 2019 16:42:42 +0900 |
parents | 63df67b6281c |
children | 29a85a427ed2 |
line wrap: on
line diff
--- a/zf.agda Mon Sep 30 21:22:07 2019 +0900 +++ b/zf.agda Sun Oct 06 16:42:42 2019 +0900 @@ -35,7 +35,7 @@ _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) _∪_ : ( A B : ZFSet ) → ZFSet - A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easier + A ∪ B = Union (A , B) {_} : ZFSet → ZFSet { x } = ( x , x ) infixr 200 _∈_