contDiff_sigmoid

Mathlib.Analysis.SpecialFunctions.Sigmoid

URI: https://scilib.ai/kg/mathlib#contDiff_sigmoid

English

The sigmoid function is infinitely differentiable: ContDiff Real WithTop.top.top sigmoid.

Русский

Сигмоида гладкая: ContDiff Real WithTop.top.top sigmoid.

LaTeX

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

Lean4

@[fun_prop]
theorem contDiff_sigmoid : ContDiff ℝ ω sigmoid :=
  analyticOn_sigmoid.contDiff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru