round_natCast_add — Mathlib

English

Same as Round Add NatCast: round((y:α) + x) = y + round x for y ∈ ℕ.

Русский

То же самое, что Round Add NatCast: round((y:α) + x) = y + round x, для y ∈ ℕ.

LaTeX

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

Lean4

@[simp]
theorem round_natCast_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x := by
  rw [add_comm, round_add_natCast, add_comm]

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