Commit 2026-04-19 20:26 a105a8cc
View on Github →feat(MeasureTheory/BorelSpace): add measurable_iSup_of_lowerSemicontinuous (#37552)
Add measurable_biSup_of_continuousOn: the supremum of a family of measurable functions parameterized by a separable pseudometric space is measurable, provided the family is continuous on the parameter set.
Upstreamed from the Carleson project.