exists_pos_mul_lt — Mathlib

English

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

Русский

Для любого a > 0 и любого b существует c > 0 such that b·c < a.

LaTeX

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

Lean4

theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a :=
  by
  have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))
  refine ⟨a / max (b + 1) 1, this, ?_⟩
  rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']
  exact lt_max_iff.2 (Or.inl <| lt_add_one _)

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