integral_Icc_eq_integral_Ioc' — Mathlib

English

Let e be a measurable equivalence X ≃ᵐ Y. Then for any f: Y → E and s ⊆ Y, ∫_s f = ∫_{e^{-1}(s)} f ∘ e.

Русский

Пусть e — измеримое эквивалентное отображение X ≃ᵐ Y. Тогда интеграл по s от f равен интегралу по предобразу e^{-1}(s) от f∘e.

LaTeX

$$$$ \\int_{y \\in s} f(y) \\, d(\\mathrm{map} \\, e \\mu)(y) = \\int_{x \\in e^{-1}(s)} f(e(x)) \\, d\\mu(x) $$$$

Lean4

theorem integral_Icc_eq_integral_Ioc' (hx : μ { x } = 0) : ∫ t in Icc x y, f t ∂μ = ∫ t in Ioc x y, f t ∂μ :=
  setIntegral_congr_set (Ioc_ae_eq_Icc' hx).symm

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