measurableEmbedding — Mathlib

English

If f: α → β is an embedding and the range of f is measurable, then f is a measurable embedding.

Русский

Если функция f: α → β является вложением и образ диапазона f измерим, то f является измеримым вложением.

LaTeX

$$(IsEmbedding\, f) \\land MeasurableSet\\,(Set.range\, f) \\Rightarrow MeasurableEmbedding\, f$$

Lean4

protected theorem measurableEmbedding {f : α → β} (h₁ : IsEmbedding f) (h₂ : MeasurableSet (range f)) :
    MeasurableEmbedding f :=
  show MeasurableEmbedding (((↑) : range f → β) ∘ h₁.toHomeomorph.toMeasurableEquiv) from
    (MeasurableEmbedding.subtype_coe h₂).comp (MeasurableEquiv.measurableEmbedding _)

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