toENat_le_ofNat — Mathlib

English

For any a and n with n ≥ 2, toENat a ≤ ofNat(n) iff a ≤ ofNat(n).

Русский

Для любого a и n с n ≥ 2, toENat a ≤ ofNat(n) тогда и только тогда, когда a ≤ ofNat(n).

LaTeX

$$$\\forall a \\in \\mathrm{Cardinal},\\ \\forall n \\in \\mathbb{N},\\ [n.\\AtLeastTwo] \\Rightarrow\\ toENat(a) \\le \\operatorname{ofNat}(n) \\iff a \\le \\operatorname{OfNat}.ofNat(n)$$$

Lean4

@[simp]
theorem toENat_le_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] : toENat a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n :=
  toENat_le_nat

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