theorem measurable_biSup_of_continuousOn {ι : Type u_1} {X : Type u_2} [PseudoEMetricSpace ι] [TopologicalSpace.SeparableSpace ι] [MeasurableSpace X] {T : Set ι} {f : ι → X → ENNReal} (mf : ∀ t ∈ T, Measurable (f t)) (cf : ∀ (x : X), ContinuousOn (fun (x_1 : ι) => f x_1 x) T) : Measurable (⨆ t ∈ T, f t)

Given T : Set ι over a separable pseudometric space ι, let f : ι → X → ℝ≥0∞ be

• measurable in x for all t ∈ T
• continuous on T for all x

Then the supremum of f over T is measurable. The proof follows https://math.stackexchange.com/a/4685735/357390.