exists_nat_mul_gt — Mathlib

English

If a ≠ 0 and b ≠ ∞, there exists 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 * a$$$

Lean4

theorem exists_nat_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n : ℕ, b < n * a :=
  (exists_nat_pos_mul_gt ha hb).imp fun _ => And.right

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