mulExpNegMulSq — Mathlib

English

If f is a continuous map, then x ↦ mulExpNegMulSq ε (f(x)) is continuous for any fixed ε.

Русский

Если f непрерывна, то x ↦ mulExpNegMulSq ε (f(x)) непрерывна для любого фиксированного ε.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem _root_.Continuous.mulExpNegMulSq {α : Type*} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) :
    Continuous (fun x => mulExpNegMulSq ε (f x)) :=
  continuous_mulExpNegMulSq.comp hf

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