Theorems · Theorem · measure theory

Embedding.comp_stronglyMeasurable_iff

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ]
  {g : β → γ} {f : α → β},
  Topology.IsEmbedding g → ((MeasureTheory.StronglyMeasurable fun x => g (f x)) ↔ MeasureTheory.StronglyMeasurable f)

If g is a topological embedding, then f is strongly measurable iff g ∘ f is.

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpace