Extr

📁 Source: Mathlib/Analysis/Normed/Module/Extr.lean

Statistics

Metric	Count
Definitions	0
Theorems norm_add_sameRay, norm_add_self, norm_add_sameRay, norm_add_self, norm_add_sameRay, norm_add_self, norm_add_sameRay, norm_add_self	8
Total	8

IsLocalMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_add_sameRay 📖	mathematical	IsLocalMax Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm SameRay Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Real.instIsStrictOrderedRing IsMaxFilter.norm_add_sameRay
norm_add_self 📖	mathematical	IsLocalMax Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	IsMaxFilter.norm_add_self

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_add_sameRay 📖	mathematical	IsLocalMaxOn Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm SameRay Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Real.instIsStrictOrderedRing IsMaxFilter.norm_add_sameRay
norm_add_self 📖	mathematical	IsLocalMaxOn Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	IsMaxFilter.norm_add_self

IsMaxFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_add_sameRay 📖	mathematical	IsMaxFilter Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm SameRay Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Real.instIsStrictOrderedRing Filter.Eventually.mono SameRay.norm_add le_imp_le_of_le_of_le norm_add_le le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
norm_add_self 📖	mathematical	IsMaxFilter Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	norm_add_sameRay SameRay.rfl Real.instIsStrictOrderedRing

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_add_sameRay 📖	mathematical	IsMaxOn Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm SameRay Real.instCommSemiring Real.partialOrder Real.instIsStrictOrderedRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Real.instIsStrictOrderedRing IsMaxFilter.norm_add_sameRay
norm_add_self 📖	mathematical	IsMaxOn Real Real.instPreorder Norm.norm SeminormedAddCommGroup.toNorm	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	IsMaxFilter.norm_add_self

---

← Back to Index