of_measurable_inverse — Mathlib

English

If a measurable embedding has a measurable inverse, then the inverse function is measurable.

Русский

Если измеримое вложение имеет измеримое обратное отображение, то обратная функция измерима.

LaTeX

$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\text{Measurable}(f^{-1})$$$

Lean4

theorem of_measurable_inverse (hf₁ : Measurable f) (hf₂ : MeasurableSet (range f)) (hg : Measurable g)
    (H : LeftInverse g f) : MeasurableEmbedding f :=
  of_measurable_inverse_on_range hf₁ hf₂ (hg.comp measurable_subtype_coe) H

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