https://github.com/math-comp/analysis/blob/1d53f980b7502ceece993994a4f3d38f6d153c4a/theories/lebesgue_integral_theory/lebesgue_integral_under.v#L49 continuity needs not be on the whole set @IshiguroYoshihiro