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

comparison 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
comparison
equal deleted inserted replaced
222:59771eb07df0 223:2e1f19c949dc
50 -- This form of regurality forces choice function 50 -- This form of regurality forces choice function
51 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 51 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
52 -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 52 -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
53 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) 53 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
54 -- another form of regularity 54 -- another form of regularity
55 ε-induction : { ψ : ZFSet → Set m} 55 -- ε-induction : { ψ : ZFSet → Set m}
56 → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) 56 -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x )
57 → (x : ZFSet ) → ψ x 57 -- → (x : ZFSet ) → ψ x
58 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 58 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
59 infinity∅ : ∅ ∈ infinite 59 infinity∅ : ∅ ∈ infinite
60 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite 60 infinity : ∀( x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
61 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) 61 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
62 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 62 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )