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

diff ordinal.agda @ 70:cd9cf8b09610

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union needs +1 space
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jun 2019 10:01:38 +0900
parents e584686a1307
children d088eb66564e
line wrap: on
line diff
--- a/ordinal.agda	Fri May 31 22:30:23 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 10:01:38 2019 +0900
@@ -22,6 +22,9 @@
     ¬ℵΦ : ¬ℵ (Φ lx) 
     ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) 
 
+--
+--    Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ...  < ℵ (Suc lv)
+--
 data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
    Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
    s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y