le_floor_add

Mathlib.Algebra.Order.Floor.Ring

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

English

For all a,b ∈ R, ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋.

Русский

Для любых a,b ∈ R верно ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋.

LaTeX

$$$$\forall a,b \in R:\ \lfloor a \rfloor + \lfloor b \rfloor \le \lfloor a + b \rfloor.$$$$

Lean4

@[bound]
theorem le_floor_add (a b : R) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋ :=
  by
  rw [le_floor, Int.cast_add]
  gcongr <;> apply floor_le

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

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

Разделы

Аффилиация

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