exists_pos_lt_mul — Mathlib

English

For any a > 0 and any b, there exists c > 0 such that b < c · a.

Русский

Для любого a > 0 и любого b существует c > 0 такой, что b < c · a.

LaTeX

$$$a>0 \Rightarrow \forall b, \exists c>0:\ b < ca$$$

Lean4

theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
  let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b;
  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]⟩

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