theorem helperForCorollary_25_7_1_deriv_continuousOn_Icc_and_monotoneOn {I : Set ℝ} (hIopen : IsOpen I) (hIconv : Convex ℝ I) {g : ℝ → ℝ} (hgconv : ConvexOn ℝ I g) (hgdiff : DifferentiableOn ℝ g I) {a b : ℝ} (_hab : a ≤ b) (hIcc : Set.Icc a b ⊆ I) : ContinuousOn (deriv g) (Set.Icc a b) ∧ MonotoneOn (deriv g) (Set.Icc a b)

Helper for Corollary 25.7.1: Theorem 25.3 gives continuity and monotonicity of the derivative on every compact subinterval once differentiability is known on the whole open interval.