Commit 2021-11-22 22:48 e59e03f1
View on Github →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.
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.