Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff zf.agda @ 223:2e1f19c949dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sepration of ordinal from OD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Aug 2019 17:57:58 +0900
parents 22d435172d1a
children 650bdad56729
line wrap: on
line diff
--- a/zf.agda	Fri Aug 09 16:54:30 2019 +0900
+++ b/zf.agda	Fri Aug 09 17:57:58 2019 +0900
@@ -52,9 +52,9 @@
      -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
      -- regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )
      -- another form of regularity
-     ε-induction : { ψ : ZFSet → Set m}
-             → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
-             → (x : ZFSet ) → ψ x
+     -- ε-induction : { ψ : ZFSet → Set m}
+     --         → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
+     --         → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite