integral_Icc_eq_integral_Ioc — Mathlib

English

If the measure μ has no atoms, then for any function f: X → E the Bochner integral of f over the closed interval [x, y] equals the integral over the half‑open interval (x, y], i.e. removing the left endpoint does not change the integral.

Русский

Если мера μ не имеет атомов, то для любой функции f: X → E интеграл Бо́чнера по замкнутому отрезку [x, y] равен интегралу по полуоткрытому интервалу (x, y], то есть удаление левой границы не меняет интеграл.

LaTeX

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

Lean4

theorem integral_Icc_eq_integral_Ioc : ∫ t in Icc x y, f t ∂μ = ∫ t in Ioc x y, f t ∂μ :=
  integral_Icc_eq_integral_Ioc' <| measure_singleton x

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