English
If f is a MeasurableEmbedding and g, g' are appropriate functions with g measurable and g' measurable, then extend f g g' is measurable.
Русский
Если f — измеримое вложение и g, g' — функции, с g измеримой и g' измеримой, то extend f g g' измерим.
LaTeX
$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\forall g,g',\\ \\text{Measurable}(g) \\Rightarrow \\text{Measurable}(g') \\Rightarrow \\text{Measurable}(\\text{extend}(f,g,g')).$$$
Lean4
theorem measurable_extend (hf : MeasurableEmbedding f) {g : α → γ} {g' : β → γ} (hg : Measurable g)
(hg' : Measurable g') : Measurable (extend f g g') :=
by
refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_
· rw [restrict_extend_range]
simpa only [rangeSplitting] using hg.comp hf.measurable_rangeSplitting
· rw [restrict_extend_compl_range]
exact hg'.comp measurable_subtype_coe
