card_lt_nat — Mathlib

English

For any ordinal o and natural n, the inequality card(o) < n is equivalent to o < n; i.e., the comparison of the cardinality of o with a natural number n matches the ordinal comparison with n treated as the corresponding finite ordinal.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem card_lt_nat {o} {n : ℕ} : card o < n ↔ o < n :=
  lt_iff_lt_of_le_iff_le nat_le_card

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