comap_subtype_coe_apply — Mathlib

English

The comap of μ along Subtype.val on t equals μ on image of t, i.e., μ((↑)'' t).

Русский

Комап μ вдоль Subtype.val на t совпадает с μ на образе t: μ((↑)'' t).

LaTeX

$$$\mathrm{comap}(\mathrm{Subtype.val}, μ)\; t = μ((\mathrm{Subtype.val})'' t).$$$

Lean4

theorem comap_subtype_coe_apply {_m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s) (μ : Measure α)
    (t : Set s) : comap (↑) μ t = μ ((↑) '' t) :=
  (MeasurableEmbedding.subtype_coe hs).comap_apply _ _

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