round_ofNat_add — Mathlib

English

For n ≥ 2, x ∈ α, round(ofNat(n) + x) = ofNat(n) + round(x).

Русский

Для n ≥ 2 и любого x верно round(ofNat(n) + x) = ofNat(n) + round(x).

LaTeX

$$$\\\\forall x \\in \\alpha, \\\\\\forall n \\in \\mathbb{N}, [n \\ge 2] \\\\\\operatorname{round}(\\operatorname{ofNat}(n) + x) = \\operatorname{ofNat}(n) + \\\\\\operatorname{round}(x).$$$

Lean4

@[simp]
theorem round_ofNat_add (n : ℕ) [n.AtLeastTwo] (x : α) : round (ofNat(n) + x) = ofNat(n) + round x :=
  round_natCast_add x n

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