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

diff Ordinals.agda @ 258:63df67b6281c

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 Wed, 04 Sep 2019 01:12:18 +0900
parents 846e0926bb89
children 304c271b3d47
line wrap: on
line diff
--- a/Ordinals.agda	Fri Aug 30 15:37:04 2019 +0900
+++ b/Ordinals.agda	Wed Sep 04 01:12:18 2019 +0900
@@ -193,9 +193,9 @@
              }
          }
 
-        TransFiniteExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
+        FExists : {m l : Level} → ( ψ : Ordinal  → Set m ) 
           → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
           → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
           → ¬ p
-        TransFiniteExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+        FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )