exists_stronglyMeasurable_extend — Mathlib

English

There exists an extension f' defined on γ such that f' ∘ g = f and f' is strongly measurable.

Русский

Существует расширение f' на γ, такое что f'∘g = f и f' сильно измеримо.

LaTeX

$$$\exists f': γ \to \beta, \mathrm{StronglyMeasurable}(f') \land (f' \circ g = f)$$$

Lean4

theorem _root_.MeasurableEmbedding.exists_stronglyMeasurable_extend {f : α → β} {g : α → γ} {_ : MeasurableSpace α}
    {_ : MeasurableSpace γ} [TopologicalSpace β] (hg : MeasurableEmbedding g) (hf : StronglyMeasurable f)
    (hne : γ → Nonempty β) : ∃ f' : γ → β, StronglyMeasurable f' ∧ f' ∘ g = f :=
  ⟨Function.extend g f fun x => Classical.choice (hne x),
    hg.stronglyMeasurable_extend hf (stronglyMeasurable_const' fun _ _ => rfl),
    funext fun _ => hg.injective.extend_apply _ _ _⟩

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