exists_pos_mul_lt — Mathlib

English

If a ≠ ∞ and b ≠ 0, there exists c > 0 such that c a < b.

Русский

Если a ≠ ∞ и b ≠ 0, существует c > 0 такое, что c a < b.

LaTeX

$$\\forall a,b ∈ ENNReal, a ≠ ∞ ∧ b ≠ 0 \\Rightarrow ∃ c > 0, c a < b$$

Lean4

protected theorem exists_pos_mul_lt (ha : a ≠ ∞) (hb₀ : b ≠ 0) : ∃ c, 0 < c ∧ c * a < b :=
  by
  obtain rfl | hb := eq_or_ne b ∞
  · exact ⟨1, by simpa [lt_top_iff_ne_top]⟩
  refine ⟨b / (a + 1), ENNReal.div_pos hb₀ (by finiteness), ENNReal.mul_lt_of_lt_div ?_⟩
  gcongr
  exacts [hb, ENNReal.lt_add_right ha one_ne_zero]

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