exists_nat_pos_inv_mul_lt — Mathlib

English

If a ≠ ∞ and b ≠ 0, there exists n > 0 such that (n)⁻¹ * a < b.

Русский

Пусть a ≠ ∞ и b ≠ 0. Существует n > 0 такое, что (n)⁻¹ · a < b.

LaTeX

$$$\\forall a,b\\in\\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq \\infty \\land b \\neq 0 \\Rightarrow \\exists n>0,\\; ((n : \\mathbb{N}) : \\mathbb{R}_{\\ge 0}^{\\infty})^{-1} * a < b$$$

Lean4

theorem exists_nat_pos_inv_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) : ∃ n > 0, ((n : ℕ) : ℝ≥0∞)⁻¹ * a < b :=
  by
  rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
  use n, npos
  rw [← ENNReal.div_eq_inv_mul]
  exact div_lt_of_lt_mul' hn

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