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

comparison zf.agda @ 258:63df67b6281c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2019 01:12:18 +0900
parents d09437fcfc7c
children 30e419a2be24
comparison
equal deleted inserted replaced
257:53b7acd63481 258:63df67b6281c
48 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t 48 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t
49 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) 49 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
50 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w ) 50 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
51 -- This form of regurality forces choice function 51 -- This form of regurality forces choice function
52 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 52 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
53 -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 53 -- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
54 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) 54 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimal x not ∈ x ∧ ( minimal x not ∩ x ≈ ∅ ) )
55 -- another form of regularity 55 -- another form of regularity
56 -- ε-induction : { ψ : ZFSet → Set m} 56 -- ε-induction : { ψ : ZFSet → Set m}
57 -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x ) 57 -- → ( {x : ZFSet } → ({ y : ZFSet } → x ∋ y → ψ y ) → ψ x )
58 -- → (x : ZFSet ) → ψ x 58 -- → (x : ZFSet ) → ψ x
59 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 59 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )