lintegral_subtype_comap — Mathlib

English

For s ⊆ α measurable, ∫ x in s f x ∂(μ.comap Subtype.val) = ∫ x in s, f x ∂μ; i.e. integration over a subtype equals integration over the original restricted to s.

Русский

Для измеримого подмножества s ⊆ α верно: ∫ x∈s f x d(μ∘Subtype.val) = ∫ x∈s f x dμ.

LaTeX

$$$$ \int⁻ x : s, f x ∂(μ.comap (↑)) = \int⁻ x in s, f x ∂μ, $$$$

Lean4

theorem lintegral_subtype_comap {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ x : s, f x ∂(μ.comap (↑)) = ∫⁻ x in s, f x ∂μ := by
  rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]

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