Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/Ordinals.agda @ 1481:42df464988e8
o<-irr reintroduce
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 30 Jun 2024 13:05:00 +0900 |
parents | 6752e2ff4dc6 |
children |
line wrap: on
line diff
--- a/src/Ordinals.agda Sun Jun 30 11:03:33 2024 +0900 +++ b/src/Ordinals.agda Sun Jun 30 13:05:00 2024 +0900 @@ -26,7 +26,7 @@ <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) - -- o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 + o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1 TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x