floor_intCast_add

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.floor_intCast_add

English

For any integer z and real a, ⌊z + a⌋ = z + ⌊a⌋.

Русский

Для любого целого z и вещественного a верно ⌊z + a⌋ = z + ⌊a⌋.

LaTeX

$$$$\forall z \in \mathbb{Z},\ a \in R:\ \left\lfloor z + a \right\rfloor = z + \left\lfloor a \right\rfloor.$$$$

Lean4

@[simp]
theorem floor_intCast_add (z : ℤ) (a : R) : ⌊↑z + a⌋ = z + ⌊a⌋ := by simpa only [add_comm] using floor_add_intCast a z

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

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

Разделы

Аффилиация

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