measure_subtype_coe_eq_zero_of_comap_eq_zero

English

If s is μ-null-measurable and t is null-measurable in μ.comap Subtype.val, then the image of t under the subtype inclusion is μ-null-measurable.

Русский

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

LaTeX

$$$\text{NullMeasurableSet } s μ \rightarrow \text{NullMeasurableSet } ((↑)'' t) μ.$$$

Lean4

theorem measure_subtype_coe_eq_zero_of_comap_eq_zero (hs : NullMeasurableSet s μ) {t : Set s}
    (ht : μ.comap Subtype.val t = 0) : μ (((↑) : s → α) '' t) = 0 :=
  eq_bot_iff.mpr <| (measure_subtype_coe_le_comap hs t).trans ht.le

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