differentiableAt_mulExpNegMulSq — Mathlib

English

For any ε ∈ ℝ and y ∈ ℝ, the function mulExpNegMulSq ε is differentiable at y.

Русский

Для любых ε ∈ ℝ и y ∈ ℝ функция mulExpNegMulSq ε дифференцируема в точке y.

LaTeX

$$$\\forall \\varepsilon \\in \\mathbb{R},\\; \\forall y \\in \\mathbb{R},\\; \\text{DifferentiableAt}(\\lambda t. mulExpNegMulSq\\,\\varepsilon\\, t)\\, y$$$

Lean4

theorem differentiableAt_mulExpNegMulSq (y : ℝ) : DifferentiableAt ℝ (mulExpNegMulSq ε) y :=
  DifferentiableAt.mul differentiableAt_fun_id (by fun_prop)

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