measurePreserving_subtype_coe — Mathlib

English

For measurable s, the natural projection from a measurable subtype to the ambient space preserves the measure comap and the restricted measure.

Русский

Для измеримого s естественное отображение из подмножества в пространство сохраняет меру comap и ограниченную меру.

LaTeX

$$$\forall s\, (\text{MeasurableSet } s) \;\; \text{MeasurePreserving } (Subtype.val : s \to α) (μ_a\,\text{comap } Subtype.val) (μ_a\text{-restrict } s)$$$

Lean4

theorem measurePreserving_subtype_coe {s : Set α} (hs : MeasurableSet s) :
    MeasurePreserving (Subtype.val : s → α) (μa.comap Subtype.val) (μa.restrict s)
    where
  measurable := measurable_subtype_coe
  map_eq := map_comap_subtype_coe hs _

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