measurableEmbedding_coe — Mathlib

English

The inclusion map I → ℝ is a measurable embedding: it is injective, measurable, and its image of measurable sets is measurable.

Русский

Вложение I → ℝ есть измеримое вложение: инъективно, измеримо и образ измеримого множества измерим.

LaTeX

$$$\text{MeasurableEmbedding}(\operatorname{Subtype.val})$ from $I$ to $\mathbb{R}$$$

Lean4

theorem measurableEmbedding_coe : MeasurableEmbedding ((↑) : I → ℝ)
    where
  injective := Subtype.val_injective
  measurable := measurable_subtype_coe
  measurableSet_image' _ := measurableSet_Icc.subtype_image

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