Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 4:c12d964a04c0
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 May 2019 11:10:53 +0900 |
| parents | e7990ff544bf |
| children | 9829ba02877f d9b704508281 |
| files | zf.agda |
| diffstat | 1 files changed, 5 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/zf.agda Sat May 11 10:47:23 2019 +0900 +++ b/zf.agda Sat May 11 11:10:53 2019 +0900 @@ -60,15 +60,15 @@ infixr 230 _∩_ _∪_ infixr 220 _⊆_ field - empty : ( x : ZFSet ) → ¬ ( ∅ ∋ x ) + empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) - power→ : ( A X t : ZFSet ) → A ∋ t → ∀ {x} {y} → _⊆_ t X {x} {y} - power← : ( A X t : ZFSet ) → ∀ {x} {y} → _⊆_ t X {x} {y} → A ∋ t + power→ : ( A t : ZFSet ) → Power A ∋ t → ∀ {x} {y} → _⊆_ t A {x} {y} + power← : ( A t : ZFSet ) → ∀ {x} {y} → _⊆_ t A {x} {y} → Power A ∋ t -- 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 = ∅ ) ) - smaller : ZFSet → ZFSet - regularity : ( x : ZFSet ) → ¬ (x ≈ ∅) → smaller x ∩ x ≈ ∅ + -- smaller : ZFSet → ZFSet + -- regularity : ( x : ZFSet ) → ¬ (x ≈ ∅) → smaller x ∩ x ≈ ∅ -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) infinite : ZFSet infinity∅ : ∅ ∈ infinite