no goals
E : Type ?u.460143
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.460239
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ (x : ℝ), x ∈ interior D → 0 < (deriv^[2]) f x
⊢ ∀ (x : ℝ), x ∈ interior (interior D) → 0 < deriv (deriv f) x
rwa [interior_interior]