sigmoid_nonneg

Mathlib.Analysis.SpecialFunctions.Sigmoid

URI: https://scilib.ai/kg/mathlib#Real.sigmoid_nonneg

English

For every x ∈ ℝ, 0 ≤ sigmoid(x).

Русский

Для каждого x ∈ ℝ выполняется 0 ≤ сигмоида(х).

LaTeX

$$$0 \le \operatorname{sigmoid}(x)$$$

Lean4

@[bound]
theorem sigmoid_nonneg (x : ℝ) : 0 ≤ sigmoid x :=
  (sigmoid_pos x).le

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

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

Разделы

Аффилиация

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