measurable_rangeSplitting — Mathlib

English

If f is a MeasurableEmbedding, then the rangeSplitting function is measurable.

Русский

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

LaTeX

$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\text{Measurable}(\\text{rangeSplitting}(f)).$$$

Lean4

theorem measurable_rangeSplitting (hf : MeasurableEmbedding f) : Measurable (rangeSplitting f) := fun s hs => by
  rwa [preimage_rangeSplitting hf.injective, ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]

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