Extrema

📁 Source: Mathlib/Analysis/Convex/Extrema.lean

Statistics

Metric	Count
Definitions	0
Theorems of_isLocalMaxOn_of_concaveOn, of_isLocalMax_of_convex_univ, of_isLocalMinOn_of_convexOn, of_isLocalMinOn_of_convexOn_Icc, of_isLocalMin_of_convex_univ	5
Total	5

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalMaxOn_of_concaveOn 📖	mathematical	Set Set.instMembership IsLocalMaxOn PartialOrder.toPreorder ConcaveOn Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	IsMaxOn	—	IsMinOn.of_isLocalMinOn_of_convexOn OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsOrderedModule OrderDual.instPosSMulReflectLE
of_isLocalMax_of_convex_univ 📖	mathematical	IsLocalMax PartialOrder.toPreorder ConcaveOn Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.univ	Preorder.toLE	—	IsMinOn.of_isLocalMin_of_convex_univ OrderDual.isOrderedAddMonoid AddCommGroup.add_comm OrderDual.instIsOrderedModule OrderDual.instPosSMulReflectLE

IsMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isLocalMinOn_of_convexOn 📖	mathematical	Set Set.instMembership IsLocalMinOn PartialOrder.toPreorder ConvexOn Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	IsMinOn	—	AffineMap.lineMap_apply_zero AffineMap.lineMap_apply_one AffineMap.lineMap_continuous instIsTopologicalAddTorsor covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Convex.segment_subset IsLocalMinOn.comp_continuousOn Continuous.continuousOn Set.left_mem_Icc zero_le_one Real.instZeroLEOneClass of_isLocalMinOn_of_convexOn_Icc one_pos NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing ConvexOn.subset ConvexOn.comp_affineMap convex_Icc IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Set.right_mem_Icc
of_isLocalMinOn_of_convexOn_Icc 📖	mathematical	Real Real.instLT IsLocalMinOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace PartialOrder.toPreorder Set.Icc Real.instPreorder ConvexOn Real.semiring Real.partialOrder Real.instAddCommMonoid AddCommGroup.toAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	IsMinOn	—	LE.le.eq_or_lt le_rfl IsMinFilter.filter_mono nhdsWithin_Icc_eq_nhdsGE instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal IsLocalMinOn.eq_1 nhdsWithin_mono Set.Ioi_subset_Ici_self Ioc_mem_nhdsGT Filter.Eventually.exists nhdsGT_neBot LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and Convex.mem_Ioc add_smul one_smul Set.left_mem_Icc LT.lt.le smul_le_smul_iff_of_pos_left IsOrderedModule.toPosSMulMono le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT IsOrderedAddMonoid.toIsOrderedCancelAddMonoid
of_isLocalMin_of_convex_univ 📖	mathematical	IsLocalMin PartialOrder.toPreorder ConvexOn Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.univ	Preorder.toLE	—	of_isLocalMinOn_of_convexOn Set.mem_univ IsLocalMin.on

---

← Back to Index