of_measurable_inverse_on_range — Mathlib

English

If there exists a measurable left-inverse on range of f, then f is a measurable embedding.

Русский

Если имеется измеримое левостороннее обратное на диапазоне f, то f — измеримое вложение.

LaTeX

$$$(\\exists g:\\mathrm{range}(f) \\to \\alpha)\\; \\text{LeftInverse } g \\; (\\mathrm{rangeFactorization}\, f) \\Rightarrow \\mathrm{MeasurableEmbedding}(f)$$$

Lean4

theorem of_measurable_inverse_on_range {g : range f → α} (hf₁ : Measurable f) (hf₂ : MeasurableSet (range f))
    (hg : Measurable g) (H : LeftInverse g (rangeFactorization f)) : MeasurableEmbedding f :=
  by
  set e : α ≃ᵐ range f :=
    ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective rangeFactorization_surjective⟩, hf₁.subtype_mk, hg⟩
  exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding

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