continuous_mulExpNegMulSq — Mathlib

English

For fixed ε ∈ ℝ, the map x ↦ mulExpNegMulSq ε x is continuous in x.

Русский

При фиксированном ε ∈ ℝ отображение x ↦ mulExpNegMulSq ε x по переменной x непрерывно.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem continuous_mulExpNegMulSq : Continuous (fun x => mulExpNegMulSq ε x) :=
  Continuous.mul continuous_id (by fun_prop)

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