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

comparison zf.agda @ 247:d09437fcfc7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix pair
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 12:27:20 +0900
parents 650bdad56729
children 63df67b6281c
comparison
equal deleted inserted replaced
246:3506f53c7d83 247:d09437fcfc7c
20 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet ) 20 (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
21 (infinite : ZFSet) 21 (infinite : ZFSet)
22 : Set (suc (n ⊔ m)) where 22 : Set (suc (n ⊔ m)) where
23 field 23 field
24 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 24 isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
25 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) 25 -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t ≈ y)
26 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) 26 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t ≈ x ) ∨ ( t ≈ y )
27 pair← : ( x y t : ZFSet ) → ( t ≈ x ) ∨ ( t ≈ y ) → (x , y) ∋ t
27 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) 28 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
28 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z 29 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
29 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) 30 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → ¬ ( (u : ZFSet ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
30 _∈_ : ( A B : ZFSet ) → Set m 31 _∈_ : ( A B : ZFSet ) → Set m
31 A ∈ B = B ∋ A 32 A ∈ B = B ∋ A