round_add_one

Mathlib.Algebra.Order.Round

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

English

For any a ∈ α, rounding a+1 equals rounding a plus 1: round(a+1) = round(a) + 1.

Русский

Для любого a ∈ α округление a+1 равно округлению a плюс 1: round(a+1) = round(a) + 1.

LaTeX

$$$\forall a \in α, \operatorname{round}(a+1) = \operatorname{round}(a) + 1$$$

Lean4

@[simp]
theorem round_add_one (a : α) : round (a + 1) = round a + 1 := by rw [← round_add_intCast a 1, cast_one]

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

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

Разделы

Аффилиация

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