card_le_nat — Mathlib

English

For any ordinal o and natural n, card(o) ≤ n is equivalent to o ≤ n; i.e., the finite bound by n in cardinal terms matches the corresponding finite bound in ordinal terms.

Русский

Для любого ординала o и натурального n, card(o) ≤ n эквивалентно o ≤ n; то есть конечное ограничение по кардиналу соответствует аналогичному ограничению по ординалу.

LaTeX

$$$\forall o\,\forall n\in\mathbb{N},\; \operatorname{card}(o) \le n \iff o \le n$$$

Lean4

@[simp]
theorem card_le_nat {o} {n : ℕ} : card o ≤ n ↔ o ≤ n :=
  le_iff_le_iff_lt_iff_lt.2 nat_lt_card

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