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

comparison zf.agda @ 269:30e419a2be24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
268:7b4a66710cdd 269:30e419a2be24
33 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 33 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
34 _⊆_ A B {x} = A ∋ x → B ∋ x 34 _⊆_ A B {x} = A ∋ x → B ∋ x
35 _∩_ : ( A B : ZFSet ) → ZFSet 35 _∩_ : ( A B : ZFSet ) → ZFSet
36 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) 36 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
37 _∪_ : ( A B : ZFSet ) → ZFSet 37 _∪_ : ( A B : ZFSet ) → ZFSet
38 A ∪ B = Union (A , B) -- Select A ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) is easier 38 A ∪ B = Union (A , B)
39 ｛_｝ : ZFSet → ZFSet 39 ｛_｝ : ZFSet → ZFSet
40 ｛ x ｝ = ( x , x ) 40 ｛ x ｝ = ( x , x )
41 infixr 200 _∈_ 41 infixr 200 _∈_
42 infixr 230 _∩_ _∪_ 42 infixr 230 _∩_ _∪_
43 infixr 220 _⊆_ 43 infixr 220 _⊆_