Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 321:a81824502ebd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Jul 2020 22:22:59 +0900 |
| parents | 21203fe0342f |
| children | fbabb20f222e |
line wrap: on
line diff
--- a/Ordinals.agda Fri Jul 03 21:58:01 2020 +0900 +++ b/Ordinals.agda Fri Jul 03 22:22:59 2020 +0900 @@ -21,7 +21,7 @@ <-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) ) - next-limit : { x : ord } → (x o< next x )∧ (¬ ((y : ord) → next x ≡ osuc y) ) + next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x @@ -58,7 +58,7 @@ <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) next-limit = IsOrdinals.next-limit (Ordinals.isOrdinal O) - + o<-dom : { x y : Ordinal } → x o< y → Ordinal o<-dom {x} _ = x