integral_Ici_eq_integral_Ioi — Mathlib

English

For no-atom μ, the Bochner integral over [x, ∞) equals the integral over (x, ∞), as the single point x has zero μ-measure.

Русский

При отсутствии атомов интеграл по [x, ∞) равен интегралу по (x, ∞), так как точка x имеет нулевую меру.

LaTeX

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

Lean4

theorem integral_Ici_eq_integral_Ioi : ∫ t in Ici x, f t ∂μ = ∫ t in Ioi x, f t ∂μ :=
  integral_Ici_eq_integral_Ioi' <| measure_singleton x

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