differentiable_mulExpNegMulSq — Mathlib

English

For every ε ∈ ℝ, the function x ↦ mulExpNegMulSq ε x is differentiable on ℝ.

Русский

Для каждого ε ∈ ℝ функция x ↦ mulExpNegMulSq ε x дифференцируема на всей ℝ.

LaTeX

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

Lean4

@[fun_prop]
theorem differentiable_mulExpNegMulSq : Differentiable ℝ (mulExpNegMulSq ε) := fun _ =>
  differentiableAt_mulExpNegMulSq _

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