ceil_add_ceil_le — Mathlib

English

For all a, b ∈ R, ceil(a) + ceil(b) ≤ ceil(a + b) + 1.

Русский

Для всех a, b ∈ R, ceil(a) + ceil(b) ≤ ceil(a + b) + 1.

LaTeX

$$$\\\\lceil a \\\\rceil + \\\\lceil b \\\\rceil \\\\le \\\\lceil a + b \\\\rceil + 1$$$

Lean4

@[bound]
theorem ceil_add_ceil_le (a b : R) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1 :=
  by
  rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
  refine (ceil_lt_add_one _).le.trans ?_
  rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
  exact le_ceil _

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