Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 186:914cc522c53a
fix extensionality
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 22 Jul 2019 18:49:38 +0900 |
parents | de3d87b7494f |
children | 1f2c8b094908 |
line wrap: on
line diff
--- a/zf.agda Mon Jul 22 18:36:45 2019 +0900 +++ b/zf.agda Mon Jul 22 18:49:38 2019 +0900 @@ -70,7 +70,7 @@ power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) - extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B + extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) -- This form of regurality forces choice function -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet