English
For any ordinal o and natural n with n ≥ 2, card(o) ≤ ofNat(n) iff o ≤ OfNat.ofNat(n).
Русский
Для ординала o и натурального n≥2, card(o) ≤ ofNat(n) эквивалентно o ≤ OfNat.ofNat(n).
LaTeX
$$$\forall o\,\forall n\in\mathbb{N},\; \operatorname{card}(o) \le \operatorname{ofNat}(n) \iff o \le \operatorname{OfNat.ofNat}(n)$$$
Lean4
theorem lt_ord_of_lt [LinearOrder α] [WellFoundedLT α] {l m : List α} {o : Ordinal} (hl : l.Sorted (· > ·))
(hm : m.Sorted (· > ·)) (hmltl : m < l) (hlt : ∀ i ∈ l, Ordinal.typein (α := α) (· < ·) i < o) :
∀ i ∈ m, Ordinal.typein (α := α) (· < ·) i < o :=
by
replace hmltl : List.Lex (· < ·) m l := hmltl
cases l with
| nil => simp at hmltl
| cons a as =>
cases m with
| nil => intro i hi; simp at hi
| cons b bs =>
intro i hi
suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa
cases hi with
| head as => exact List.head_le_of_lt hmltl
| tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_sorted_cons hm _ hi) (List.head_le_of_lt hmltl))
