English
Let o be an ordinal and n a natural number with n ≥ 2. Then the finite cardinal corresponding to n is strictly less than the cardinality of o if and only if the ordinal corresponding to n is strictly less than o; i.e. (ofNat n) < card(o) is equivalent to (OfNat.ofNat n) < o.
Русский
Пусть o — ординал, а n — натуральное число, такое что n ≥ 2. Тогда конечно соответствующее n число как кардинал меньше кардинала o тогда и только тогда, когда ординал n меньше o; то есть (ofNat n) < card(o) эквивалентно (OfNat.ofNat n) < o.
LaTeX
$$$\forall o\ \forall n\in\mathbb{N}\ (n\ge 2)\;:\; (\operatorname{ofNat}(n) : \operatorname{Cardinal}) < \operatorname{card}(o) \;\iff\; (\operatorname{OfNat.ofNat} n) < o$$$
Lean4
@[simp]
theorem ofNat_lt_card {o} {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Cardinal) < card o ↔ (OfNat.ofNat n : Ordinal) < o :=
nat_lt_card
