round_add_natCast — Mathlib

English

In a linearly ordered ring with floor, adding a natural number to x commutes with rounding: round(x + y) = round(x) + y for all x and y ∈ ℕ.

Русский

При условии упорядоченного кольца и floor округление сохраняется при добавлении натурального числа: round(x + y) = round(x) + y, для всех x и y ∈ ℕ.

LaTeX

$$$\\\\forall x \in \\alpha, \\\\\\forall y \in \\mathbb{N}, \\\\\\operatorname{round}(x + y) = \\\\\\operatorname{round}(x) + y.$$$

Lean4

@[simp]
theorem round_add_natCast (x : α) (y : ℕ) : round (x + y) = round x + y :=
  mod_cast round_add_intCast x y

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