round_sub_natCast

Mathlib.Algebra.Order.Round

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

English

For y ∈ ℕ, round(x − y) = round(x) − y.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem round_sub_natCast (x : α) (y : ℕ) : round (x - y) = round x - y :=
  mod_cast round_sub_intCast x y

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

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

Разделы

Аффилиация

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