integral_Ico_eq_integral_Ioo — Mathlib

English

If μ has no atoms, then the Bochner integral over [x, y) equals that over (x, y), since the left endpoint x contributes zero measure.

Русский

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

LaTeX

$$$$\\int_{t \\in Ico\\,x\\,y} f(t)\\,d\\mu = \\int_{t \\in Ioo\\,x\\,y} f(t)\\,d\\mu.$$$$

Lean4

theorem integral_Ico_eq_integral_Ioo : ∫ t in Ico x y, f t ∂μ = ∫ t in Ioo x y, f t ∂μ :=
  integral_Ico_eq_integral_Ioo' <| measure_singleton x

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