Sigmoid

📁 Source: Mathlib/Analysis/SpecialFunctions/Sigmoid.lean

Statistics

Metric	Count
Definitions sigmoid, sigmoid, sigmoid	3
Theorems sigmoid, sigmoid', sigmoid, sigmoid, sigmoid, sigmoid, sigmoid, sigmoid, sigmoid, deriv_sigmoid, hasDerivAt_sigmoid, range_sigmoid, sigmoid_def, sigmoid_inj, sigmoid_injective, sigmoid_le, sigmoid_le_iff, sigmoid_le_one, sigmoid_lt, sigmoid_lt_iff, sigmoid_lt_one, sigmoid_monotone, sigmoid_mul_rexp_neg, sigmoid_neg, sigmoid_nonneg, sigmoid_pos, sigmoid_strictMono, sigmoid_zero, tendsto_sigmoid_atBot, tendsto_sigmoid_atTop, isEmbedding_sigmoid, analyticAt_sigmoid, analyticOnNhd_sigmoid, analyticOn_sigmoid, analyticWithinAt_sigmoid, contDiff_sigmoid, continuous_sigmoid, differentiableAt_sigmoid, differentiable_sigmoid, measurableEmbedding_sigmoid, measurableEmbedding_sigmoid_comp_embeddingReal, continuous_sigmoid, range_sigmoid, sigmoid_inj, sigmoid_injective, sigmoid_le, sigmoid_le_iff, sigmoid_lt, sigmoid_lt_iff, sigmoid_lt_one, sigmoid_monotone, sigmoid_neg, sigmoid_pos, sigmoid_strictMono, tendsto_sigmoid_atBot, tendsto_sigmoid_atTop	56
Total	59

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	AnalyticAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Real.sigmoid	—	comp analyticAt_sigmoid
sigmoid' 📖	mathematical	AnalyticAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Real.sigmoid	—	sigmoid

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Real.sigmoid	—	AnalyticOnNhd.comp_analyticOn analyticOnNhd_sigmoid Set.mapsTo_univ

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Real.sigmoid	—	AnalyticAt.comp analyticAt_sigmoid

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	AnalyticWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	Real.sigmoid	—	AnalyticAt.comp_analyticWithinAt analyticAt_sigmoid

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Top.top WithTop ENat WithTop.top	Real.sigmoid	—	comp contDiff_sigmoid

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.pseudoMetricSpace	Real.sigmoid	—	comp continuous_sigmoid

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	Real.sigmoid	—	comp differentiable_sigmoid

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sigmoid 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace	Real.sigmoid	—	comp differentiableAt_sigmoid

OrderEmbedding

Definitions

Name	Category	Theorems
sigmoid 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
sigmoid 📖	CompOp	38 math math: hasDerivAt_sigmoid, ContDiff.sigmoid, DifferentiableAt.sigmoid, Continuous.sigmoid, tendsto_sigmoid_atTop, differentiableAt_sigmoid, sigmoid_neg, sigmoid_le, AnalyticOn.sigmoid, sigmoid_nonneg, AnalyticAt.sigmoid', sigmoid_lt_iff, sigmoid_inj, sigmoid_def, analyticOnNhd_sigmoid, sigmoid_mul_rexp_neg, sigmoid_pos, tendsto_sigmoid_atBot, sigmoid_injective, sigmoid_lt, analyticAt_sigmoid, Differentiable.sigmoid, AnalyticAt.sigmoid, sigmoid_monotone, sigmoid_le_one, sigmoid_le_iff, analyticWithinAt_sigmoid, analyticOn_sigmoid, sigmoid_zero, deriv_sigmoid, AnalyticWithinAt.sigmoid, AnalyticOnNhd.sigmoid, range_sigmoid, sigmoid_strictMono, sigmoid_lt_one, differentiable_sigmoid, contDiff_sigmoid, continuous_sigmoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_sigmoid 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace sigmoid instMul instSub instOne	—	HasDerivAt.deriv hasDerivAt_sigmoid
hasDerivAt_sigmoid 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal sigmoid instMul instSub instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing sigmoid_neg sigmoid_mul_rexp_neg sigmoid_def Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval mul_neg neg_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval mul_one Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one exp_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos HasDerivAt.inv HasDerivAt.const_add HasDerivAt.exp hasDerivAt_neg'
range_sigmoid 📖	mathematical	—	Set.range Real sigmoid Set.Ioo instPreorder instZero instOne	—	subset_antisymm Set.instAntisymmSubset sigmoid_pos sigmoid_lt_one sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid one_lt_inv_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instZeroLEOneClass neg_neg exp_log add_sub_cancel inv_inv
sigmoid_def 📖	mathematical	—	sigmoid Real instInv instAdd instOne exp instNeg	—	—
sigmoid_inj 📖	mathematical	—	sigmoid	—	sigmoid_injective
sigmoid_injective 📖	mathematical	—	Real sigmoid	—	StrictMono.injective sigmoid_strictMono
sigmoid_le 📖	mathematical	Real instLE	sigmoid	—	sigmoid_le_iff
sigmoid_le_iff 📖	mathematical	—	Real instLE sigmoid	—	StrictMono.le_iff_le sigmoid_strictMono
sigmoid_le_one 📖	mathematical	—	Real instLE sigmoid instOne	—	LT.lt.le sigmoid_lt_one
sigmoid_lt 📖	mathematical	Real instLT	sigmoid	—	sigmoid_lt_iff
sigmoid_lt_iff 📖	mathematical	—	Real instLT sigmoid	—	StrictMono.lt_iff_lt sigmoid_strictMono
sigmoid_lt_one 📖	mathematical	—	Real instLT sigmoid instOne	—	inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instZeroLEOneClass lt_add_iff_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le exp_pos
sigmoid_monotone 📖	mathematical	—	Monotone Real instPreorder sigmoid	—	StrictMono.monotone sigmoid_strictMono
sigmoid_mul_rexp_neg 📖	mathematical	—	Real instMul sigmoid exp instNeg	—	sigmoid_neg sigmoid_def Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one exp_pos Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero
sigmoid_neg 📖	mathematical	—	sigmoid Real instNeg instSub instOne	—	Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one neg_neg Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one exp_pos Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial add_comm add_sub_cancel_right add_mul Distrib.rightDistribClass add_neg_cancel exp_zero
sigmoid_nonneg 📖	mathematical	—	Real instLE instZero sigmoid	—	LT.lt.le sigmoid_pos
sigmoid_pos 📖	mathematical	—	Real instLT instZero sigmoid	—	inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one exp_pos
sigmoid_strictMono 📖	mathematical	—	StrictMono Real instPreorder sigmoid	—	inv_strictAnti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one exp_pos add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd exp_strictMono neg_lt_neg
sigmoid_zero 📖	mathematical	—	sigmoid Real instZero instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero exp_zero Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat
tendsto_sigmoid_atBot 📖	mathematical	—	Filter.Tendsto Real sigmoid Filter.atBot instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero	—	Filter.Tendsto.inv_tendsto_atTop instIsStrictOrderedRing instOrderTopologyReal Filter.Tendsto.add_atTop instIsOrderedAddMonoid tendsto_const_nhds tendsto_exp_comp_atTop Filter.tendsto_neg_atBot_atTop
tendsto_sigmoid_atTop 📖	mathematical	—	Filter.Tendsto Real sigmoid Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instOne	—	add_zero inv_one Filter.Tendsto.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Filter.Tendsto.const_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_exp_comp_nhds_zero Filter.tendsto_neg_atTop_atBot instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_zero

Topology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEmbedding_sigmoid 📖	mathematical	—	IsEmbedding Real Set.Elem unitInterval UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceSubtype Set Set.instMembership unitInterval.sigmoid	—	OrderEmbedding.isEmbedding_of_ordConnected instOrderTopologyReal orderTopology_of_ordConnected Set.ordConnected_Icc Set.ordConnected_of_Ioo Real.instIsOrderedRing Set.Ioo_subset_Ioo unitInterval.range_sigmoid

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_sigmoid 📖	mathematical	—	AnalyticAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sigmoid	—	AnalyticAt.fun_inv AnalyticAt.fun_add analyticAt_const AnalyticAt.rexp' AnalyticAt.fun_neg analyticAt_id ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Real.exp_pos
analyticOnNhd_sigmoid 📖	mathematical	—	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sigmoid Set.univ	—	analyticAt_sigmoid
analyticOn_sigmoid 📖	mathematical	—	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sigmoid Set.univ	—	AnalyticOnNhd.analyticOn analyticOnNhd_sigmoid
analyticWithinAt_sigmoid 📖	mathematical	—	AnalyticWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.sigmoid	—	AnalyticAt.analyticWithinAt analyticAt_sigmoid
contDiff_sigmoid 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Top.top WithTop ENat WithTop.top Real.sigmoid	—	AnalyticOn.contDiff analyticOn_sigmoid
continuous_sigmoid 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.sigmoid	—	Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Differentiable.sigmoid differentiable_id
differentiableAt_sigmoid 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.sigmoid	—	differentiable_sigmoid
differentiable_sigmoid 📖	mathematical	—	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.sigmoid	—	ContDiff.differentiable_one ContDiff.of_le contDiff_sigmoid le_top
measurableEmbedding_sigmoid 📖	mathematical	—	MeasurableEmbedding Real Set.Elem unitInterval Real.measurableSpace Subtype.instMeasurableSpace Set Set.instMembership unitInterval.sigmoid	—	Topology.IsEmbedding.measurableEmbedding Real.borelSpace Subtype.borelSpace Topology.isEmbedding_sigmoid Real.instIsOrderedRing measurableSet_Ioo Subtype.opensMeasurableSpace BorelSpace.opensMeasurable Subtype.instOrderClosedTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid unitInterval.range_sigmoid
measurableEmbedding_sigmoid_comp_embeddingReal 📖	mathematical	—	MeasurableEmbedding Set.Elem Real unitInterval Subtype.instMeasurableSpace Set Set.instMembership Real.measurableSpace unitInterval.sigmoid MeasureTheory.embeddingReal	—	MeasurableEmbedding.comp measurableEmbedding_sigmoid MeasureTheory.measurableEmbedding_embeddingReal

unitInterval

Definitions

Name	Category	Theorems
sigmoid 📖	CompOp	18 math math: sigmoid_le_iff, sigmoid_lt, sigmoid_strictMono, measurableEmbedding_sigmoid, measurableEmbedding_sigmoid_comp_embeddingReal, continuous_sigmoid, range_sigmoid, sigmoid_neg, sigmoid_injective, tendsto_sigmoid_atTop, sigmoid_lt_iff, sigmoid_monotone, sigmoid_inj, sigmoid_pos, Topology.isEmbedding_sigmoid, tendsto_sigmoid_atBot, sigmoid_lt_one, sigmoid_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_sigmoid 📖	mathematical	—	Continuous Real Set.Elem unitInterval UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceSubtype Set Set.instMembership sigmoid	—	continuous_sigmoid
range_sigmoid 📖	mathematical	—	Set.range Set.Elem Real unitInterval sigmoid Set.Ioo Subtype.preorder Real.instPreorder Set Set.instMembership Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	—	Real.instIsOrderedRing sigmoid.eq_1 Set.Subtype.range_coind Real.range_sigmoid Set.ext
sigmoid_inj 📖	mathematical	—	sigmoid	—	sigmoid_injective
sigmoid_injective 📖	mathematical	—	Real Set.Elem unitInterval sigmoid	—	StrictMono.injective sigmoid_strictMono
sigmoid_le 📖	mathematical	Real Real.instLE	Set.Elem unitInterval Set Set.instMembership sigmoid	—	sigmoid_le_iff
sigmoid_le_iff 📖	mathematical	—	Set.Elem Real unitInterval Real.instLE Set Set.instMembership sigmoid	—	Real.sigmoid_le_iff
sigmoid_lt 📖	mathematical	Real Real.instLT	Set.Elem unitInterval Set Set.instMembership sigmoid	—	sigmoid_lt_iff
sigmoid_lt_iff 📖	mathematical	—	Set.Elem Real unitInterval Real.instLT Set Set.instMembership sigmoid	—	Real.sigmoid_lt_iff
sigmoid_lt_one 📖	mathematical	—	Set.Elem Real unitInterval Real.instLT Set Set.instMembership sigmoid Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.sigmoid_lt_one
sigmoid_monotone 📖	mathematical	—	Monotone Real Set.Elem unitInterval Real.instPreorder Subtype.preorder Set Set.instMembership sigmoid	—	StrictMono.monotone sigmoid_strictMono
sigmoid_neg 📖	mathematical	—	sigmoid Real Real.instNeg symm	—	Real.sigmoid_neg
sigmoid_pos 📖	mathematical	—	Set.Elem Real unitInterval Real.instLT Set Set.instMembership Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing sigmoid	—	Real.sigmoid_pos
sigmoid_strictMono 📖	mathematical	—	StrictMono Real Set.Elem unitInterval Real.instPreorder Subtype.preorder Set Set.instMembership sigmoid	—	Real.sigmoid_strictMono
tendsto_sigmoid_atBot 📖	mathematical	—	Filter.Tendsto Real Set.Elem unitInterval sigmoid Filter.atBot Real.instPreorder nhds instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing tendsto_subtype_rng Real.tendsto_sigmoid_atBot
tendsto_sigmoid_atTop 📖	mathematical	—	Filter.Tendsto Real Set.Elem unitInterval sigmoid Filter.atTop Real.instPreorder nhds instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing tendsto_subtype_rng Real.tendsto_sigmoid_atTop

---

← Back to Index