Mathlib Map

Theorems · Definition · real analysis

Real.sigmoid

ℝ → ℝ

The sigmoid function from ℝ to ℝ.

Defined in
Mathlib.Analysis.SpecialFunctions.Sigmoid
Cited by
39 results in Mathlib
Foundations
Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

unitInterval.sigmoid · cited by 19unitInterval.sigmoidanalyticAt_sigmoid · cited by 5analyticAt_sigmoidReal.sigmoid_strictMono · cited by 5Real.sigmoid_strictMonoReal.sigmoid_lt_one · cited by 3Real.sigmoid_lt_oneReal.sigmoid_neg · cited by 3Real.sigmoid_negReal.sigmoid_pos · cited by 3Real.sigmoid_poscontinuous_sigmoid · cited by 2continuous_sigmoidReal.sigmoid_def · cited by 2Real.sigmoid_defReal.sigmoid_le_iff · cited by 2Real.sigmoid_le_iffReal.sigmoid_lt_iff · cited by 2Real.sigmoid_lt_iffanalyticOnNhd_sigmoid · cited by 2analyticOnNhd_sigmoidunitInterval.range_sigmoid · cited by 2unitInterval.range_sigmoidcontDiff_sigmoid · cited by 2contDiff_sigmoiddifferentiable_sigmoid · cited by 2differentiable_sigmoidReal.sigmoid_injective · cited by 1Real.sigmoid_injectiveReal · cited by 25697RealReal.exp · cited by 871Real.expReal.sigmoidCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement and proof · cited by 25,697
  • Real.expproof · cited by 871

Cited by40

Results whose statement or proof uses this declaration.