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

comparison zf.agda @ 78:9a7a64b2388c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite and replacement begin no Russel Pradox
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 10:19:52 +0900
parents 75ba8cf64707
children c8b79d303867
comparison
equal deleted inserted replaced
77:75ba8cf64707 78:9a7a64b2388c
51 _⊆_ A B {x} = A ∋ x → B ∋ x 51 _⊆_ A B {x} = A ∋ x → B ∋ x
52 _∩_ : ( A B : ZFSet ) → ZFSet 52 _∩_ : ( A B : ZFSet ) → ZFSet
53 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) ) 53 A ∩ B = Select A ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
54 _∪_ : ( A B : ZFSet ) → ZFSet 54 _∪_ : ( A B : ZFSet ) → ZFSet
55 A ∪ B = Union (A , B) 55 A ∪ B = Union (A , B)
56 ｛_｝ : ZFSet → ZFSet
57 ｛ x ｝ = ( x , x )
56 infixr 200 _∈_ 58 infixr 200 _∈_
57 infixr 230 _∩_ _∪_ 59 infixr 230 _∩_ _∪_
58 infixr 220 _⊆_ 60 infixr 220 _⊆_
59 field 61 field
60 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x ) 62 empty : ∀( x : ZFSet ) → ¬ ( ∅ ∋ x )
66 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) 68 -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
67 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 69 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
68 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) ) 70 regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )
69 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) 71 -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
70 infinity∅ : ∅ ∈ infinite 72 infinity∅ : ∅ ∈ infinite
71 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ Select X ( λ y → x ≈ y )) ∈ infinite 73 infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite
72 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ ) 74 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet } → ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈ Select X ψ )
73 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) 75 -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
74 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ ) 76 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( ψ x ∈ Replace X ψ )
75 77
76 record ZF {n m : Level } : Set (suc (n ⊔ m)) where 78 record ZF {n m : Level } : Set (suc (n ⊔ m)) where