Theorems · Theorem · convex and discrete geometry

IsMinOn.of_isLocalMinOn_of_convexOn_Icc

∀ {β : Type u_2} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] [inst_3 : Module ℝ β]
  [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {f : ℝ → β} {a b : ℝ},
  a < b → IsLocalMinOn f (Set.Icc a b) a → ConvexOn ℝ (Set.Icc a b) f → IsMinOn f (Set.Icc a b) a

Helper lemma for the more general case: IsMinOn.of_isLocalMinOn_of_convexOn.

Defined in

Mathlib.Analysis.Convex.Extrema

Cited by

1 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupPartialOrderIsOrderedAddMonoidModuleIsOrderedModulePosSMulReflectLE