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

comparison zf.agda @ 186:914cc522c53a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix extensionality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2019 18:49:38 +0900
parents de3d87b7494f
children 1f2c8b094908
comparison
equal deleted inserted replaced
185:a002ce0346dd 186:914cc522c53a
68 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 68 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
69 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 69 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
70 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x} 70 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x}
71 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t 71 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t
72 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) 72 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
73 extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B 73 extensionality : { A B w : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → ( A ∈ w ⇔ B ∈ w )
74 -- This form of regurality forces choice function 74 -- This form of regurality forces choice function
75 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 75 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
76 -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 76 -- minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
77 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) 77 -- regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
78 -- another form of regularity 78 -- another form of regularity