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

comparison zf.agda @ 166:ea0e7927637a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use double negation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Jul 2019 10:52:31 +0900
parents ebac6fa116fa
children de3d87b7494f
comparison
equal deleted inserted replaced
165:d16b8bf29f4f 166:ea0e7927637a
22 open import Relation.Nullary 22 open import Relation.Nullary
23 open import Relation.Binary 23 open import Relation.Binary
24 24
25 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 25 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
26 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) 26 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
27
28 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
29 double-neg A notnot = notnot A
27 30
28 infixr 130 _∧_ 31 infixr 130 _∧_
29 infixr 140 _∨_ 32 infixr 140 _∨_
30 infixr 150 _⇔_ 33 infixr 150 _⇔_
31 34
62 infixr 230 _∩_ _∪_ 65 infixr 230 _∩_ _∪_
63 infixr 220 _⊆_ 66 infixr 220 _⊆_
64 field 67 field
65 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 68 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
66 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 69 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
67 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x} 70 power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → t ∋ x → ¬ ¬ ( A ∋ x ) -- _⊆_ t A {x}
68 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t 71 power← : ∀( A t : ZFSet ) → ( ∀ {x} → _⊆_ t A {x}) → Power A ∋ t
69 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) 72 -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
70 extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B 73 extensionality : { A B : ZFSet } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
71 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 74 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
72 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 75 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet