LineDeriv

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

Statistics

Metric	Count
Definitions LineDeriv	1
Theorems hasLineDerivAt_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, hasLineDerivWithinAt_eq_zero, lineDerivWithin_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, hasLineDerivWithinAt_eq_zero, lineDerivWithin_eq_zero, lineDeriv_eq_zero, hasLineDerivAt_eq_zero, hasLineDerivWithinAt_eq_zero, lineDerivWithin_eq_zero, lineDeriv_eq_zero	20
Total	21

IsExtrFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	—	IsExtrFilter Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Tendsto AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsLocalExtr.hasDerivAt_eq_zero comp_tendsto zero_smul add_zero
lineDeriv_eq_zero 📖	mathematical	IsExtrFilter Real Real.instPreorder Filter.Tendsto AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	hasLineDerivAt_eq_zero LineDifferentiableAt.hasLineDerivAt lineDeriv_zero_of_not_lineDifferentiableAt

IsExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	—	IsExtrOn Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsExtrFilter.hasLineDerivAt_eq_zero Filter.tendsto_principal
hasLineDerivWithinAt_eq_zero 📖	—	IsExtrOn Real Real.instPreorder HasLineDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	hasLineDerivAt_eq_zero HasLineDerivWithinAt.hasLineDerivAt'
lineDerivWithin_eq_zero 📖	mathematical	IsExtrOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDerivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	hasLineDerivWithinAt_eq_zero LineDifferentiableWithinAt.hasLineDerivWithinAt lineDerivWithin_zero_of_not_lineDifferentiableWithinAt
lineDeriv_eq_zero 📖	mathematical	IsExtrOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	IsExtrFilter.lineDeriv_eq_zero Filter.tendsto_principal

IsLocalExtr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	mathematical	IsLocalExtr Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	Real.instZero	—	IsExtrFilter.hasLineDerivAt_eq_zero Continuous.tendsto' Continuous.fun_add continuous_const Continuous.smul continuous_id' zero_smul add_zero
lineDeriv_eq_zero 📖	mathematical	IsLocalExtr Real Real.instPreorder	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Pi.instZero Real.instZero	—	IsExtrFilter.lineDeriv_eq_zero Continuous.tendsto' Continuous.fun_add continuous_const Continuous.smul continuous_id' zero_smul add_zero

IsLocalMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	mathematical	IsLocalMax Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	Real.instZero	—	IsLocalExtr.hasLineDerivAt_eq_zero
lineDeriv_eq_zero 📖	mathematical	IsLocalMax Real Real.instPreorder	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Pi.instZero Real.instZero	—	IsLocalExtr.lineDeriv_eq_zero

IsLocalMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	mathematical	IsLocalMin Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	Real.instZero	—	IsLocalExtr.hasLineDerivAt_eq_zero
lineDeriv_eq_zero 📖	mathematical	IsLocalMin Real Real.instPreorder	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Pi.instZero Real.instZero	—	IsLocalExtr.lineDeriv_eq_zero

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	—	IsMaxOn Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsExtrOn.hasLineDerivAt_eq_zero isExtr
hasLineDerivWithinAt_eq_zero 📖	—	IsMaxOn Real Real.instPreorder HasLineDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsExtrOn.hasLineDerivWithinAt_eq_zero isExtr
lineDerivWithin_eq_zero 📖	mathematical	IsMaxOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDerivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	IsExtrOn.lineDerivWithin_eq_zero isExtr
lineDeriv_eq_zero 📖	mathematical	IsMaxOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	IsExtrOn.lineDeriv_eq_zero isExtr

IsMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt_eq_zero 📖	—	IsMinOn Real Real.instPreorder HasLineDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsExtrOn.hasLineDerivAt_eq_zero isExtr
hasLineDerivWithinAt_eq_zero 📖	—	IsMinOn Real Real.instPreorder HasLineDerivWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—	IsExtrOn.hasLineDerivWithinAt_eq_zero isExtr
lineDerivWithin_eq_zero 📖	mathematical	IsMinOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDerivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	IsExtrOn.lineDerivWithin_eq_zero isExtr
lineDeriv_eq_zero 📖	mathematical	IsMinOn Real Real.instPreorder Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField	—	IsExtrOn.lineDeriv_eq_zero isExtr

(root)

Definitions

Name	Category	Theorems
LineDeriv 📖	CompData	—

---

← Back to Index