subtype_coe — Mathlib

English

If s is measurable, then the inclusion map from s to α is a MeasurableEmbedding.

Русский

Если множество s измеримо, то инклюзивное отображение из s в α — измеримое вложение.

LaTeX

$$$\\text{MeasurableSet}(s) \\Rightarrow \\text{MeasurableEmbedding}(\\text{Subtype.val}).$$$

Lean4

theorem subtype_coe (hs : MeasurableSet s) : MeasurableEmbedding ((↑) : s → α)
    where
  injective := Subtype.coe_injective
  measurable := measurable_subtype_coe
  measurableSet_image' := fun _ => MeasurableSet.subtype_image hs

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