range_sigmoid — Mathlib

English

The image of the sigmoid on the unit interval is the open interval (0,1); in particular, all values strictly between 0 and 1 are attained.

Русский

Образ сигмоиды на единичном отрезке равен открытому интервалу (0,1); каждое значение в (0,1) достигается.

LaTeX

$$$\mathrm{range}\bigl(\operatorname{unitInterval.sigmoid}\bigr) = \mathrm{Ioo}(0,1)$$$

Lean4

theorem range_sigmoid : range unitInterval.sigmoid = Ioo 0 1 :=
  by
  rw [sigmoid, Subtype.range_coind, Real.range_sigmoid]
  ext
  simp

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