ofNat_le_card — Mathlib

English

For any o and n, (ofNat n) ≤ card o ↔ (OfNat n) ≤ o; i.e., the natural embedding respects cardinal order.

Русский

Для любого o и n, (ofNat n) ≤ card o ↔ (OfNat n) ≤ o; т.е. естественное вложение сохраняет кардинальную ординальную структуру.

LaTeX

$$$(\\mathrm{ofNat}(n)) \\le \\mathrm{card}(o) \\iff (\\mathrm{OfNat}(n)) \\le o$$$

Lean4

@[simp]
theorem ofNat_le_card {o} {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Cardinal) ≤ card o ↔ (OfNat.ofNat n : Ordinal) ≤ o :=
  nat_le_card

Похожие утверждения