Theorems · Theorem · convex and discrete geometry

ConvexOn.continuousOn_Icc

∀ {f : ℝ → ℝ} {y z : ℝ},
  ConvexOn ℝ (Set.Icc y z) f →
    y < z → ContinuousWithinAt f (Set.Ici y) y → ContinuousWithinAt f (Set.Iic z) z → ContinuousOn f (Set.Icc y z)

Defined in

Mathlib.Analysis.Convex.Continuous

Cited by

1 results in Mathlib

Foundations

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