Measurability through an inducing map #
For an inducing map f : α → β between Borel spaces, the Borel σ-algebra of α is the
pullback of the Borel σ-algebra of β along f. Hence a map g into α is measurable exactly
when f ∘ g is. Unlike MeasurableEmbedding.measurable_comp_iff, this needs no measurability
of the range of f: a topological embedding with non-measurable range still detects
measurability of maps into its domain.
Main results #
theorem
Topology.IsInducing.measurable_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[TopologicalSpace α]
[MeasurableSpace α]
[BorelSpace α]
[TopologicalSpace β]
[MeasurableSpace β]
[BorelSpace β]
[MeasurableSpace γ]
{f : α → β}
(hf : IsInducing f)
{g : γ → α}
:
For an inducing map f between Borel spaces, a map g into the domain of f is measurable
exactly when f ∘ g is.