restrict_lintegral_eq_lintegral_restrict

English

Restricting the function to s and taking lintegral with μ is the same as taking lintegral with μ restricted to s.

Русский

Ограничение функции f до множества s и взятие линеграль по μ эквивалентно взятию линеграль по μ, ограниченной на s.

LaTeX

$$$(\\restrict f s).lintegral μ = f.lintegral(μ.restrict s)$$$

Lean4

theorem restrict_lintegral_eq_lintegral_restrict (f : α →ₛ ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
    (restrict f s).lintegral μ = f.lintegral (μ.restrict s) := by rw [f.restrict_lintegral hs, lintegral_restrict]

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