Theorems · Theorem · measure theory

MeasurableEmbedding.exists_stronglyMeasurable_extend

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {x : MeasurableSpace α} {x_1 : MeasurableSpace γ}
  [inst : TopologicalSpace β],
  MeasurableEmbedding g →
    MeasureTheory.StronglyMeasurable f →
      (∀ (a : γ), Nonempty β) → ∃ f', MeasureTheory.StronglyMeasurable f' ∧ f' ∘ g = f

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace