Basic

📁 Source: Mathlib/Analysis/Calculus/LocalExtr/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv_eq_zero, fderiv_eq_zero, hasDerivAt_eq_zero, hasFDerivAt_eq_zero, deriv_eq_zero, fderiv_eq_zero, hasDerivAt_eq_zero, hasFDerivAt_eq_zero, fderivWithin_eq_zero, fderivWithin_nonpos, hasFDerivWithinAt_eq_zero, hasFDerivWithinAt_nonpos, deriv_eq_zero, fderiv_eq_zero, hasDerivAt_eq_zero, hasFDerivAt_eq_zero, fderivWithin_eq_zero, fderivWithin_nonneg, hasFDerivWithinAt_eq_zero, hasFDerivWithinAt_nonneg, mem_posTangentConeAt_of_frequently_mem, mem_posTangentConeAt_of_segment_subset, one_mem_posTangentConeAt_iff_frequently, one_mem_posTangentConeAt_iff_mem_closure, posTangentConeAt_mono, posTangentConeAt_univ, sub_mem_posTangentConeAt_of_segment_subset	27
Total	27

IsLocalExtr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_eq_zero 📖	mathematical	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instZero	—	elim IsLocalMin.deriv_eq_zero IsLocalMax.deriv_eq_zero
fderiv_eq_zero 📖	mathematical	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder	fderiv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	elim IsLocalMin.fderiv_eq_zero IsLocalMax.fderiv_eq_zero
hasDerivAt_eq_zero 📖	mathematical	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	Real.instZero	—	elim ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsLocalMin.hasDerivAt_eq_zero IsLocalMax.hasDerivAt_eq_zero
hasFDerivAt_eq_zero 📖	mathematical	IsLocalExtr Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.zero RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	elim IsLocalMin.hasFDerivAt_eq_zero IsLocalMax.hasFDerivAt_eq_zero

IsLocalMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_eq_zero 📖	mathematical	IsLocalMax Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instZero	—	hasDerivAt_eq_zero DifferentiableAt.hasDerivAt deriv_zero_of_not_differentiableAt
fderiv_eq_zero 📖	mathematical	IsLocalMax Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder	fderiv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_eq_zero DifferentiableAt.hasFDerivAt fderiv_zero_of_not_differentiableAt
hasDerivAt_eq_zero 📖	mathematical	IsLocalMax Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	Real.instZero	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal neg_eq_zero IsLocalMin.hasDerivAt_eq_zero neg Real.instIsOrderedAddMonoid HasDerivAt.neg
hasFDerivAt_eq_zero 📖	mathematical	IsLocalMax Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.zero RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	instIsTopologicalAddGroupReal neg_eq_zero IsLocalMin.hasFDerivAt_eq_zero neg Real.instIsOrderedAddMonoid HasFDerivAt.neg

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderivWithin_eq_zero 📖	mathematical	IsLocalMaxOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousLinearMap.funLike fderivWithin Real.instZero	—	hasFDerivWithinAt_eq_zero DifferentiableWithinAt.hasFDerivWithinAt fderivWithin_zero_of_not_differentiableWithinAt
fderivWithin_nonpos 📖	mathematical	IsLocalMaxOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	Real.instLE DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousLinearMap.funLike fderivWithin Real.instZero	—	hasFDerivWithinAt_nonpos DifferentiableWithinAt.hasFDerivWithinAt fderivWithin_zero_of_not_differentiableWithinAt le_refl
hasFDerivWithinAt_eq_zero 📖	mathematical	IsLocalMaxOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instZero	—	le_antisymm hasFDerivWithinAt_nonpos map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
hasFDerivWithinAt_nonpos 📖	mathematical	IsLocalMaxOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup	Real.instLE DFunLike.coe StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instZero	—	exists_fun_of_mem_tangentConeAt tendsto_nhdsWithin_iff Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_const_nhds Filter.Eventually.mono Filter.Tendsto.eventually add_zero mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal HasFDerivWithinAt.lim IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul

IsLocalMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_eq_zero 📖	mathematical	IsLocalMin Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	deriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.instZero	—	hasDerivAt_eq_zero DifferentiableAt.hasDerivAt deriv_zero_of_not_differentiableAt
fderiv_eq_zero 📖	mathematical	IsLocalMin Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder	fderiv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.zero	—	hasFDerivAt_eq_zero DifferentiableAt.hasFDerivAt fderiv_zero_of_not_differentiableAt
hasDerivAt_eq_zero 📖	mathematical	IsLocalMin Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	Real.instZero	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal one_mul DFunLike.congr_fun hasFDerivAt_eq_zero hasDerivAt_iff_hasFDerivAt
hasFDerivAt_eq_zero 📖	mathematical	IsLocalMin Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.zero RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	ContinuousLinearMap.ext IsLocalMinOn.hasFDerivWithinAt_eq_zero on HasFDerivAt.hasFDerivWithinAt posTangentConeAt_univ Set.mem_univ

IsLocalMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderivWithin_eq_zero 📖	mathematical	IsLocalMinOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousLinearMap.funLike fderivWithin Real.instZero	—	hasFDerivWithinAt_eq_zero DifferentiableWithinAt.hasFDerivWithinAt fderivWithin_zero_of_not_differentiableWithinAt
fderivWithin_nonneg 📖	mathematical	IsLocalMinOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	Real.instLE Real.instZero DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.pseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace ContinuousLinearMap.funLike fderivWithin	—	hasFDerivWithinAt_nonneg DifferentiableWithinAt.hasFDerivWithinAt fderivWithin_zero_of_not_differentiableWithinAt le_refl
hasFDerivWithinAt_eq_zero 📖	mathematical	IsLocalMinOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsLocalMaxOn.hasFDerivWithinAt_eq_zero neg Real.instIsOrderedAddMonoid HasFDerivWithinAt.neg
hasFDerivWithinAt_nonneg 📖	mathematical	IsLocalMinOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Set Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup	Real.instLE Real.instZero DFunLike.coe StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLocalMaxOn.hasFDerivWithinAt_nonpos neg HasFDerivWithinAt.neg

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_posTangentConeAt_of_frequently_mem 📖	mathematical	Filter.Frequently Real Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField nhdsWithin Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder	posTangentConeAt NormedAddCommGroup.toAddCommGroup	—	mem_tangentConeAt_of_add_smul_mem NNReal.instContinuousSMulOfReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.frequently_iff_neBot Filter.frequently_map NNReal.map_coe_nhdsGT NNReal.coe_zero Filter.tendsto_id' LE.le.trans inf_le_left nhdsGT_le_nhdsNE
mem_posTangentConeAt_of_segment_subset 📖	mathematical	Set Set.instHasSubset segment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup	—	add_sub_cancel_left sub_mem_posTangentConeAt_of_segment_subset
one_mem_posTangentConeAt_iff_frequently 📖	mathematical	—	Real Set Set.instMembership posTangentConeAt Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne Filter.Frequently nhdsWithin Set.Ioi Real.instPreorder	—	one_mem_posTangentConeAt_iff_mem_closure mem_closure_iff_frequently frequently_nhdsWithin_iff Set.inter_comm
one_mem_posTangentConeAt_iff_mem_closure 📖	mathematical	—	Real Set Set.instMembership posTangentConeAt Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne closure Set.instInter Set.Ioi Real.instPreorder	—	exists_fun_of_mem_tangentConeAt add_zero Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds mem_closure_of_tendsto Filter.mp_mem Filter.Tendsto.eventually_const_lt instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Filter.univ_mem' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono contravariant_lt_of_covariant_le pos_of_mul_pos_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mem_posTangentConeAt_of_frequently_mem mul_one Filter.frequently_map map_add_left_nhds_zero instIsTopologicalAddGroupReal mem_closure_iff_frequently
posTangentConeAt_mono 📖	mathematical	—	Monotone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	tangentConeAt_mono
posTangentConeAt_univ 📖	mathematical	—	posTangentConeAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.univ	—	tangentConeAt_univ NNReal.instContinuousSMulOfReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instNeBotNhdsWithinComplSetSingletonOfNontrivial NNReal.instOrderTopology NNReal.instDenselyOrdered
sub_mem_posTangentConeAt_of_segment_subset 📖	mathematical	Set Set.instHasSubset segment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField	Set.instMembership posTangentConeAt NormedAddCommGroup.toAddCommGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_mem_posTangentConeAt_of_openSegment_subset IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasSubset.Subset.trans Set.instIsTransSubset openSegment_subset_segment

---

← Back to Index