round_add_intCast — Mathlib

English

For x ∈ α and y ∈ ℤ, round(x+y) = round(x) + y. Rounding commutes with integer shifts.

Русский

Для x ∈ α и y ∈ ℤ, round(x+y) = round(x) + y. Округление сохраняет при добавлении целого.

LaTeX

$$$\forall x \in α, \forall y \in \mathbb{Z}, \operatorname{round}(x+y) = \operatorname{round}(x) + y$$$

Lean4

@[simp]
theorem round_add_intCast (x : α) (y : ℤ) : round (x + y) = round x + y := by
  rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast, ← apply_ite₂, ite_self]

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