card_lt_ofNat — Mathlib

English

Let o be an ordinal and n a natural number with n ≥ 2. Then card(o) < ofNat(n) if and only if o < OfNat.ofNat(n); i.e., the finite cardinal bound corresponds exactly to the finite ordinal bound.

Русский

Пусть o — ординал и n — натуральное число с n ≥ 2. Тогда card(o) < ofNat(n) если и только если o < OfNat.ofNat(n); то есть конечное ограничение по кардиналу точно соответствует конечному ограничению по ординалу.

LaTeX

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

Lean4

@[simp]
theorem card_lt_ofNat {o} {n : ℕ} [n.AtLeastTwo] : card o < ofNat(n) ↔ o < OfNat.ofNat n :=
  card_lt_nat

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