ceil_lt_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 \\tfrac{b}{1-b} \\rceil \\le a \\Rightarrow \\lceil a \\rceil < b a$$$

Lean4

theorem ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉ / b < a) : ⌈a⌉ < b * a :=
  by
  obtain hab | hba := le_total a (b - 1)⁻¹
  ·
    calc
      ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈a⌉ < a + 1 := ceil_lt_add_one _
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

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