∀ {β : 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