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