Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 37:f10ceee99d00
¬ ( y c< x ) → x ≡ od∅
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 23 May 2019 13:48:27 +0900 |
| parents | c9ad0d97ce41 |
| children | 83b13f1f4f42 |
line wrap: on
line diff
--- a/zf.agda Thu May 23 02:32:02 2019 +0900 +++ b/zf.agda Thu May 23 13:48:27 2019 +0900 @@ -71,8 +71,8 @@ -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) - minimul : ZFSet → ( ZFSet ∧ ZFSet ) - regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( proj1 ( minimul x ) ∈ x ∧ ( proj1 ( minimul x ) ∩ x ≈ ∅ ) ) + minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet + regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) infinity∅ : ∅ ∈ infinite infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ Select X ( λ y → x ≈ y )) ∈ infinite