tendsto_const_mul_rpow_nhds_zero_of_pos

English

If c ≠ ∞ and y > 0, then as x → 0, c·x^y → 0 in ENNReal.

Русский

Если c ≠ ∞ и y > 0, то при x → 0, c·x^y → 0 в ENNReal.

LaTeX

$$$\\\\text{If } c \\\\neq \\infty \\\\text{ and } y > 0, \\\\; (x \\mapsto c \\cdot x^y) \\\\to 0 \\\\text{ as } x \\to 0$ in ENNReal.$$

Lean4

theorem tendsto_const_mul_rpow_nhds_zero_of_pos {c : ℝ≥0∞} (hc : c ≠ ∞) {y : ℝ} (hy : 0 < y) :
    Tendsto (fun x : ℝ≥0∞ => c * x ^ y) (𝓝 0) (𝓝 0) :=
  by
  convert ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
  · simp [hy]
  · exact Or.inr hc

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