exists_nat_pos_mul_gt — Mathlib

English

If a ≠ 0 and b ≠ ∞, there exists a positive natural n such that b < n * a.

Русский

Пусть a ≠ 0 и b ≠ ∞. Существует положительное натуральное число n такое, что b < n·a.

LaTeX

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

Lean4

theorem exists_nat_pos_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n > 0, b < (n : ℕ) * a :=
  let ⟨n, hn⟩ := ENNReal.exists_nat_gt (div_lt_top hb ha).ne
  ⟨n, Nat.cast_pos.1 ((zero_le _).trans_lt hn), by rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]⟩

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