Theorem: ConvexOn.continuousOn (LeanCamCombi/ConvexContinuous.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
f : E → ℝ
hf : ConvexOn ℝ s f
⊢ ContinuousOn f (intrinsicInterior ℝ s)
Tactic:
classical
sorry
State after:
no goals

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
f : E → ℝ
hf : ConvexOn ℝ s f
⊢ ContinuousOn f (intrinsicInterior ℝ s)
Tactic:
sorry
State after:
no goals