English
If f is a MeasurableEmbedding and g is measurable and for each β there exists a γ, there exists a β → γ measurable extension g' with g' ∘ f = g.
Русский
Если f — измеримое вложение, а g измеримо и для каждого β существует γ, то существует измеримое продолжение g' такого вида, что g' ∘ f = g.
LaTeX
$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\forall g:\\alpha \\to \\gamma,\\text{Measurable}(g) \\Rightarrow (\\forall a:\\beta, \\text{Nonempty}(\\gamma)) \\Rightarrow \\exists g':\\beta \\to \\gamma,\\ \\text{Measurable}(g') \\land (g' \\circ f = g).$$$
Lean4
theorem exists_measurable_extend (hf : MeasurableEmbedding f) {g : α → γ} (hg : Measurable g) (hne : β → Nonempty γ) :
∃ g' : β → γ, Measurable g' ∧ g' ∘ f = g :=
⟨extend f g fun x => Classical.choice (hne x), hf.measurable_extend hg (measurable_const' fun _ _ => rfl),
funext fun _ => hf.injective.extend_apply _ _ _⟩
