ceil_le_mul — Mathlib

English

If 1 < b and ⌈(b−1)⁻¹⌉/b ≤ a, then ⌈a⌉ ≤ b a.

Русский

Если 1 < b и ⌈(b−1)⁻¹⌉/b ≤ a, то ⌈a⌉ ≤ b a.

LaTeX

$$$1 < b \\land \\lceil (b-1)^{-1} \\rceil / b \\le a \\Rightarrow \\lceil a \\rceil \\le b a$$$

Lean4

theorem ceil_le_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉ / b ≤ a) : ⌈a⌉ ≤ b * a :=
  by
  obtain rfl | hba := hba.eq_or_lt
  · rw [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity
  · exact (ceil_lt_mul hb hba).le

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