Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 258:63df67b6281c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 04 Sep 2019 01:12:18 +0900 |
| parents | d09437fcfc7c |
| children | 30e419a2be24 |
line wrap: on
line diff
--- a/zf.agda Fri Aug 30 15:37:04 2019 +0900 +++ b/zf.agda Wed Sep 04 01:12:18 2019 +0900 @@ -50,8 +50,8 @@ 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 - -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) + -- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet + -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimal x not ∈ x ∧ ( minimal x not ∩ x ≈ ∅ ) ) -- another form of regularity -- ε-induction : { ψ : ZFSet → Set m} -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x )