integral_Iic_eq_integral_Iio — Mathlib

English

If μ has no atoms, then the Bochner integral over [x, ∞) equals that over (−∞, x) with appropriate orientation; more simply, the left endpoint x has zero measure so removing it does not change the integral.

Русский

Если μ не имеет атомов, то интеграл по [x, ∞) совпадает с интегралом по (−∞, x], левая граница не вносит вклад.

LaTeX

$$$$\\int_{t \\in Iic\\,x} f(t)\\,d\\mu = \\int_{t \\in Iio\\,x} f(t)\\,d\\mu.$$$$

Lean4

theorem integral_Iic_eq_integral_Iio : ∫ t in Iic x, f t ∂μ = ∫ t in Iio x, f t ∂μ :=
  integral_Iic_eq_integral_Iio' <| measure_singleton x

Похожие утверждения