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

diff OD.agda @ 348:08d94fec239c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit ordinal and possible OD bound
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 07:59:17 +0900
parents 06f10815d0b3
children 811152bf2f47
line wrap: on
line diff
--- a/OD.agda	Mon Jul 13 22:40:37 2020 +0900
+++ b/OD.agda	Tue Jul 14 07:59:17 2020 +0900
@@ -390,7 +390,7 @@
         u : (y : Ordinal ) → HOD
         u y = Union (ord→od y , (ord→od y , ord→od y))
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-        lemma {o∅} iφ = proj1  next-limit
+        lemma {o∅} iφ = x<nx
         lemma (isuc {y} x) = lemma2 where
             lemma0 : y o< next o∅
             lemma0 = lemma x