eq_zero_of_le_mul_pow — Mathlib

English

If x ≤ ε · r^n for all n and r < 1, then x = 0.

Русский

Если x ≤ ε · r^n для всех n и r < 1, то x = 0.

LaTeX

$$$\\\\forall x, r \\\\in \\\\mathbb{R}_{\\\\ge 0}∞, \\\\forall ε \\\\in \\\\mathbb{R}_{\\\\ge 0}, \\\\ r < 1 \\\\Rightarrow (\\\\forall n, x \\\\le ε \\\\cdot r^n) \\\\Rightarrow x = 0.$$$

Lean4

theorem eq_zero_of_le_mul_pow {x r : ℝ≥0∞} {ε : ℝ≥0} (hr : r < 1) (h : ∀ n : ℕ, x ≤ ε * r ^ n) : x = 0 :=
  by
  rw [← nonpos_iff_eq_zero]
  refine ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * r ^ n) (x := atTop) ?_ h
  rw [← mul_zero (M₀ := ℝ≥0∞) (a := ε)]
  exact Tendsto.const_mul (tendsto_pow_atTop_nhds_zero_of_lt_one hr) (Or.inr coe_ne_top)

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