le_floor_add_floor — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[bound]
theorem le_floor_add_floor (a b : R) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋ :=
  by
  rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
  refine le_trans ?_ (sub_one_lt_floor _).le
  rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
  exact floor_le _

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