Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 302:304c271b3d47
HOD and reduction mapping of Ordinals
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 28 Jun 2020 18:09:04 +0900 |
parents | 63df67b6281c |
children | b172ab9f12bc |
line wrap: on
line diff
--- a/Ordinals.agda Wed Jun 24 14:05:38 2020 +0900 +++ b/Ordinals.agda Sun Jun 28 18:09:04 2020 +0900 @@ -20,6 +20,7 @@ ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) + is-limit : { x : ord } → Dec ( ¬ ((y : ord) → x ≡ osuc y) ) TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x