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

comparison zf.agda @ 72:f39f1a90d154

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 Sat, 01 Jun 2019 14:43:05 +0900
parents cd9cf8b09610
children dd430a95610f
comparison
equal deleted inserted replaced
71:d088eb66564e 72:f39f1a90d154
50 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z) 50 -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
51 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B ) 51 pair : ( A B : ZFSet ) → ( (A , B) ∋ A ) ∧ ( (A , B) ∋ B )
52 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u)) 52 -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x ∧ (z ∈ u))
53 union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet 53 union-u : ( X z : ZFSet ) → Union X ∋ z → ZFSet
54 union→ : ( X z u : ZFSet ) → ((Union X ∋ u ) ∧ (u ∋ z )) → Union X ∋ z 54 union→ : ( X z u : ZFSet ) → ((Union X ∋ u ) ∧ (u ∋ z )) → Union X ∋ z
55 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z ) 55 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
56 _∈_ : ( A B : ZFSet ) → Set m 56 _∈_ : ( A B : ZFSet ) → Set m
57 A ∈ B = B ∋ A 57 A ∈ B = B ∋ A
58 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m 58 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set m
59 _⊆_ A B {x} = A ∋ x → B ∋ x 59 _⊆_ A B {x} = A ∋ x → B ∋ x
60 _∩_ : ( A B : ZFSet ) → ZFSet 60 _∩_ : ( A B : ZFSet ) → ZFSet