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

$$$$ (hb: 1 < b) \Rightarrow (hba: ⌈(b-1)^{-1}⌉_+ / b \le a) \Rightarrow \lceil a \rceil_+ \le b \cdot 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 [mul_div_cancel₀, cast_le, ceil_le]
    · exact _root_.div_le_self (by positivity) hb.le
    · positivity
  · exact (ceil_lt_mul hb hba).le

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