sigmoid — Mathlib

English

The sigmoid function is continuously differentiable of all orders; in particular, it is smooth.

Русский

Сигмоида непрерывно дифференцируема во всех порядках; следовательно, она гладкая.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{R}}^{\omega}(\operatorname{sigmoid})$$$

Lean4

theorem sigmoid {x : E} (fa : AnalyticWithinAt ℝ f s x) : AnalyticWithinAt ℝ (sigmoid ∘ f) s x :=
  analyticAt_sigmoid.comp_analyticWithinAt fa

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