range_sigmoid — Mathlib

English

The range of sigmoid is the open interval (0,1).

Русский

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

LaTeX

$$$\operatorname{range}(\operatorname{sigmoid}) = (0,1)$$$

Lean4

theorem range_sigmoid : range Real.sigmoid = Ioo 0 1 :=
  by
  refine subset_antisymm ?_ fun x hx ↦ ?_
  · rintro - ⟨x, rfl⟩
    simp only [mem_Ioo]
    bound
  · replace hx : 0 < x⁻¹ - 1 := by rwa [sub_pos, one_lt_inv_iff₀]
    exact ⟨-(log (x⁻¹ - 1)), by simp [sigmoid_def, exp_log hx]⟩

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