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

diff 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
line wrap: on
line diff
--- a/zf.agda	Sat Jun 01 10:23:53 2019 +0900
+++ b/zf.agda	Sat Jun 01 14:43:05 2019 +0900
@@ -52,7 +52,7 @@
      -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
      union-u : ( X z : ZFSet  ) → Union X ∋ z → ZFSet
      union→ : ( X z u : ZFSet ) → ((Union X ∋ u )  ∧ (u ∋ z )) → Union X ∋ z
-     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (Union X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ z )
+     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ z )
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m