ofNat_nonneg' — Mathlib

English

For every n ≥ 2, the image of n under the natural numeral embedding is nonnegative: 0 ≤ (ofNat(n) : α).

Русский

Для каждого n ≥ 2 образ числа n в α неотрицателен: 0 ≤ (ofNat(n) : α).

LaTeX

$$$\forall n \in \mathbb{N}, n \ge 2 \Rightarrow 0 \le (\mathrm{ofNat}(n) : \alpha).$$$

Lean4

/-- See also `Nat.ofNat_nonneg`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem ofNat_nonneg' (n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α) :=
  cast_nonneg' n

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