tendsto_mulExpNegMulSq — Mathlib

English

For every ε ∈ ℝ, mulExpNegMulSq ε is a differentiable map ℝ → ℝ.

Русский

Для каждого ε ∈ ℝ функция mulExpNegMulSq ε : ℝ → ℝ дифференцируема.

LaTeX

$$$\\forall \\varepsilon \\in \\mathbb{R},\\; \\text{Differentiable}(\\lambda x. mulExpNegMulSq\\,\\varepsilon\\, x)$$$

Lean4

/-- For fixed `x : ℝ`, the mapping `mulExpNegMulSq ε x` converges pointwise to `x` as `ε → 0` -/
theorem tendsto_mulExpNegMulSq {x : ℝ} : Tendsto (fun ε => mulExpNegMulSq ε x) (𝓝 0) (𝓝 x) :=
  by
  have : x = (fun ε : ℝ => mulExpNegMulSq ε x) 0 := by simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]
  nth_rw 2 [this]
  apply Continuous.tendsto (Continuous.mul continuous_const (by fun_prop))

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