round_intCast_add

Mathlib.Algebra.Order.Round

URI: https://scilib.ai/kg/mathlib#round_intCast_add

English

For y ∈ ℤ, round(y + x) = y + round(x).

Русский

Для y ∈ ℤ верно round(y + x) = y + round(x).

LaTeX

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

Lean4

@[simp]
theorem round_intCast_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x := by
  rw [add_comm, round_add_intCast, add_comm]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru