map_comap_subtype_coe — Mathlib

English

For any measurable s, the map of comap Subtype.val μ by Subtype.val equals the restricted μ to s.

Русский

Для любого измеримого s отображение комап по Subtype.val μ равно ограниченной μ на s.

LaTeX

$$$\mathrm{map} \; \mathrm{Subtype.val} (\mathrm{comap} \; \mathrm{Subtype.val} \; μ) = μ.restrict s$$$

Lean4

theorem map_comap_subtype_coe {m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (μ : Measure α) :
    (comap (↑) μ).map ((↑) : s → α) = μ.restrict s := by
  rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]

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