mul_lt_floor — Mathlib

English

If b > 0 and b < 1, and ⌈b/(1−b)⌉ ≤ a, then b·a < ⌊a⌋_+.

Русский

Если 0<b<1 и ⌈b/(1−b)⌉ ≤ a, то b·a < ⌊a⌋_+.

LaTeX

$$$$ hb_0: 0 < b, hb: b < 1, hba: \lceil \frac{b}{1-b} \rceil_+ \le a \Rightarrow b \cdot a < \lfloor a \rfloor_+ $$$$

Lean4

theorem mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊ := by
  calc
    b * a < b * (⌊a⌋₊ + 1) := by gcongr; apply lt_floor_add_one
    _ ≤ ⌊a⌋₊ :=
      by
      rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith), ← ceil_le]
      exact le_floor hba

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