subtype_coe — Mathlib

English

If s is μ-null-measurable and t is null-measurable with respect to μ.comap Subtype.val, then the image of t under the inclusion map has μ-null-measurability.

Русский

Если s нулемеряемо по μ и t нулемеряемо по μ.comap Subtype.val, то образ t при включении имеет нулемеряемость по μ.

LaTeX

$$$\text{NullMeasurableSet } s μ \rightarrow \big( \text{NullMeasurableSet } t (μ.comap Subtype.val) \rightarrow \text{NullMeasurableSet } ((↑)'' t) μ \big).$$$

Lean4

theorem subtype_coe {t : Set s} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t (μ.comap Subtype.val)) :
    NullMeasurableSet (((↑) : s → α) '' t) μ :=
  NullMeasurableSet.image _ μ Subtype.coe_injective (fun _ => MeasurableSet.nullMeasurableSet_subtype_coe hs) ht

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