English
Given a measurable embedding g, extending f along g yields a strongly measurable extension.
Русский
Пусть g --- измеримое вложение. Расширение f вдоль g строго измеримо.
LaTeX
$$$\text{MeasurableEmbedding}(g) \Rightarrow \mathrm{StronglyMeasurable}(f) \Rightarrow \mathrm{StronglyMeasurable}(\mathrm{extend}\ g\ f\ g')$$$
Lean4
@[measurability]
theorem _root_.MeasurableEmbedding.stronglyMeasurable_extend {f : α → β} {g : α → γ} {g' : γ → β}
{mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [TopologicalSpace β] (hg : MeasurableEmbedding g)
(hf : StronglyMeasurable f) (hg' : StronglyMeasurable g') : StronglyMeasurable (Function.extend g f g') :=
by
refine ⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), ?_⟩
intro x
by_cases hx : ∃ y, g y = x
· rcases hx with ⟨y, rfl⟩
simpa only [SimpleFunc.extend_apply, hg.injective, Injective.extend_apply] using hf.tendsto_approx y
· simpa only [hx, SimpleFunc.extend_apply', not_false_iff, extend_apply'] using hg'.tendsto_approx x
