integral_subtype_comap — Mathlib

English

For measurable sets s and any f, the integral over the subtype equals the integral over s: ∫ x: s f x = ∫ x∈s f x.

Русский

Для измеримого множества s интеграл по подтипу равен интегралу по s: ∫ x: s f x = ∫ x∈s f x.

LaTeX

$$$$\int x : s, f x \partial(Measure.Subtype.measureSpace.volume) = \int x ∈ s, f x.$$$$

Lean4

theorem integral_subtype_comap {α} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → G) :
    ∫ x : s, f (x : α) ∂(Measure.comap Subtype.val μ) = ∫ x in s, f x ∂μ :=
  by
  rw [← map_comap_subtype_coe hs]
  exact ((MeasurableEmbedding.subtype_coe hs).integral_map _).symm

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