integral_Ici_eq_integral_Ioi' — Mathlib

English

For a real-valued f and threshold R, the integrals over Ici x and Ioi x are equal when μ({x}) = 0.

Русский

Для порога R и функции f, интегралы по Ici x и Ioi x совпадают при μ({x}) = 0.

LaTeX

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

Lean4

theorem integral_Ici_eq_integral_Ioi' (hx : μ { x } = 0) : ∫ t in Ici x, f t ∂μ = ∫ t in Ioi x, f t ∂μ :=
  setIntegral_congr_set (Ioi_ae_eq_Ici' hx).symm

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