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

diff src/OrdUtil.agda @ 789:a08c456d49d0

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, 03 Aug 2022 01:49:34 +0900
parents d92ad9e365b6
children 171123c92007
line wrap: on
line diff
--- a/src/OrdUtil.agda	Tue Aug 02 16:09:00 2022 +0900
+++ b/src/OrdUtil.agda	Wed Aug 03 01:49:34 2022 +0900
@@ -84,7 +84,8 @@
 ... | case1 x=y = subst ( λ k → ox o< k ) (x=y) x<y
 ... | case2 y<z = ordtrans x<y y<z
 
-open _∧_
+o∅≤z : {z : Ordinal } → o∅ o< (osuc z)
+o∅≤z {z} = b<x→0<x ( <-osuc )
 
 osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
 proj2 (osuc2 x y) lt = osucc lt