theorem ERealFunction.convex_epigraph_iSup {H : Type u} {I : Type v} [AddCommGroup H] [Module ℝ H] (f : I → H → EReal) (hconv : ∀ (i : I), Convex ℝ (epigraph (f i))) : Convex ℝ (epigraph (⨆ (i : I), f i))

Proposition 8.16: the pointwise supremum of a family of extended-real-valued functions with convex epigraphs again has convex epigraph, hence is convex.