mathlib3

e59e03f1 - feat(measure_theory/integral/interval_integral): add an alternative definition (#10380)

feat(measure_theory/integral/interval_integral): add an alternative definition (#10380) Prove that `∫ x in a..b, f x ∂μ = sgn a b • ∫ x in Ι a b, f x ∂μ`, where `sgn a b = if a ≤ b then 1 else -1`.