ceil_div_ceil_inv_sub_one — Mathlib

English

For a field k with 0 < b < 1 and a ≥ ⌈b/(1−b)⌉, ba < ⌊a⌋.

Русский

Для поля k с 0 < b < 1 и a ≥ ⌈b/(1−b)⌉ верно ba < ⌊a⌋.

LaTeX

$$$0 < b < 1 \\land a \\ge \\lceil \\tfrac{b}{1-b} \\rceil \\Rightarrow b a < \\lfloor a \\rfloor$$$

Lean4

theorem ceil_div_ceil_inv_sub_one (ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉ :=
  by
  obtain rfl | ha := ha.eq_or_lt
  · simp
  have : 0 < a - 1 := by linarith
  refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
  rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub, ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]
  convert ceil_lt_add_one (R := k) _ using 1
  field_simp
  abel

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