Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison zf.agda @ 51:83b13f1f4f42
...
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 ) |