ceil_lt_mul — Mathlib

English

If x ≥ 50/19, then ⌈x⌉ < (69/50) x.

Русский

Пусть x ≥ 50/19. Тогда ⌈x⌉ < (69/50) x.

LaTeX

$$$$ \\lceil x \\rceil < \\tfrac{69}{50} x \\quad\\text{for}\\quad x \\ge \\tfrac{50}{19}. $$$$

Lean4

theorem ceil_lt_mul {x : ℝ} (hx : 50 / 19 ≤ x) : (⌈x⌉₊ : ℝ) < 1.38 * x :=
  by
  refine (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le ?_
  rw [← le_sub_iff_add_le', ← sub_one_mul]
  have : (1.38 : ℝ) = 69 / 50 := by norm_num
  rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ← div_eq_inv_mul, one_le_div]
  norm_num1

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