Continuity and differentiability of convex functions

TheoremContinuity (continuity and differentiability of convex functions)#

Mathlib states this as ConvexOn.continuousOn.

ConvexOn.continuousOn.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E}
  {f : E → ℝ} [FiniteDimensional ℝ E] (hC : IsOpen C) (hf : ConvexOn ℝ C f) : ContinuousOn f C

Sources

• Mathlib documentation: ConvexOn.continuousOn
• Source of ConvexOn.continuousOn in Mathlib/Analysis/Convex/Continuous.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Convexity › continuity and differentiability of convex functions

MathlibConvexOn.continuousOn

Uses 15

Statement usesConvex function · Finite-dimensionality · Normed vector space over a normed field

Proof usesAffine span · Cardinal · Characteristic zero · Convex hull of a subset of an affine real space · Euclidean affine space · Linear independence · Metric structure · Order topology · The Triangle Inequality · Topological module · Topological ring · Topology of a metric space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.