exists_nnreal_pos_mul_lt — Mathlib

English

If a ≠ ∞ and b ≠ 0, there exists n > 0 with ↑(n) · a < b, where ↑ denotes the natural embedding of NNReal into ENNReal.

Русский

Если a ≠ ∞ и b ≠ 0, существует n > 0 такое, что ↑n · a < b, где ↑ — встраивание NNReal в ENNReal.

LaTeX

$$$\\exists n>0, \\; \\uparrow(n) * a < b$$$

Lean4

theorem exists_nnreal_pos_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ↑(n : ℝ≥0) * a < b :=
  by
  rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩
  use (n : ℝ≥0)⁻¹
  simp [*, npos.ne']

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