Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 70:cd9cf8b09610
Union needs +1 space
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jun 2019 10:01:38 +0900 |
| parents | 93abc0133b8a |
| children | f39f1a90d154 |
line wrap: on
line diff
--- a/zf.agda Fri May 31 22:30:23 2019 +0900 +++ b/zf.agda Sat Jun 01 10:01:38 2019 +0900 @@ -50,8 +50,9 @@ -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) - union-u : ( y z : ZFSet ) → ZFSet - union-iso : ( X z : ZFSet ) → (Union X ∋ z ) ⇔ ((Union X ∋ union-u X z ) ∧ (union-u X z ∋ z )) + union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet + union→ : ( X z u : ZFSet ) → ((Union X ∋ u ) ∧ (u ∋ z )) → Union X ∋ z + union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z ) _∈_ : ( A B : ZFSet ) → Set m A ∈ B = B ∋ A _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m