integral_Icc_eq_integral_Ico — Mathlib

English

If μ has no atoms, then for any f: X → E the Bochner integrals over the closed interval [x, y] and the half‑open interval [x, y) are equal (the right endpoint is left unchanged by equality of measures up to a point).

Русский

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

LaTeX

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

Lean4

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

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