setIntegral_restrict — Mathlib

English

A measurable set s can be used to restrict the integral of f with respect to κ a to t, via intersection.

Русский

Измеримое множество s используется для ограничения интеграла по κ a до t через пересечение с s.

LaTeX

$$$\\int x \\in t f(x) \\, d\\kappa.restrict hs (a) = \\int x \\in t \\cap s f(x) \\, d\\kappa(a)$$$

Lean4

@[simp]
theorem setIntegral_restrict (hs : MeasurableSet s) (t : Set β) :
    ∫ x in t, f x ∂κ.restrict hs a = ∫ x in t ∩ s, f x ∂κ a := by rw [restrict_apply, Measure.restrict_restrict' hs]

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