sigmoid — Mathlib

English

The sigmoid function defines an order-preserving embedding of the real line into the unit interval.

Русский

Функция сигмоиды задает отображение, сохраняющее порядок, из ℝ в единичный интервал.

LaTeX

$$$\operatorname{sigmoid}: \mathbb{R} \hookrightarrow \mathbb{I}$ is an order-embedding$$

Lean4

/-- The Sigmoid function as an `OrderEmbedding` from `ℝ` to `I`. -/
noncomputable def sigmoid : ℝ ↪o I :=
  OrderEmbedding.ofStrictMono unitInterval.sigmoid unitInterval.sigmoid_strictMono

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