mul_lt_floor — Mathlib

English

Let 0 < b < 1 and ⌈b/(1−b)⌉ ≤ a. Then ba < ⌊a⌋ in any suitable ordered field.

Русский

Пусть 0 < b < 1 и ⌈b/(1−b)⌉ ≤ a. Тогда ba < ⌊a⌋ в подходящем упорядоченном поле.

LaTeX

$$$0 < b < 1 \\quad\\text{and}\\quad \\lceil \\tfrac{b}{1-b} \\rceil \\le a\\quad\\Rightarrow\\quad b 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
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith), ← ceil_le, le_floor]

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