round_add_ofNat — Mathlib

English

If n ≥ 2 is a natural number and x is in the ring, then round(n + x) = n + round(x).

Русский

Пусть n ≥ 2 — натуральное число. Тогда round(n + x) = n + round(x).

LaTeX

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

Lean4

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

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