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

comparison zf.agda @ 51:83b13f1f4f42

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 Mon, 27 May 2019 15:00:45 +0900
parents f10ceee99d00
children 33fb8228ace9
comparison
equal deleted inserted replaced
50:7cb32d22528c 51:83b13f1f4f42
55 _∈_ : ( A B : ZFSet ) → Set m 55 _∈_ : ( A B : ZFSet ) → Set m
56 A ∈ B = B ∋ A 56 A ∈ B = B ∋ A
57 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 57 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
58 _⊆_ A B {x} = A ∋ x → B ∋ x 58 _⊆_ A B {x} = A ∋ x → B ∋ x
59 _∩_ : ( A B : ZFSet ) → ZFSet 59 _∩_ : ( A B : ZFSet ) → ZFSet
60 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) 60 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
61 _∪_ : ( A B : ZFSet ) → ZFSet 61 _∪_ : ( A B : ZFSet ) → ZFSet
62 A ∪ B = Select (A , B) ( λ x → ( A ∋ x ) ∨ ( B ∋ x ) ) 62 A ∪ B = Union (A , B)
63 infixr 200 _∈_ 63 infixr 200 _∈_
64 infixr 230 _∩_ _∪_ 64 infixr 230 _∩_ _∪_
65 infixr 220 _⊆_ 65 infixr 220 _⊆_
66 field 66 field
67 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 67 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )