Theorems · Theorem · general topology

MeasurableSet.image_of_measurable_injOn

∀ {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace α] {s : Set γ} {f : γ → α}
  [MeasurableSpace.CountablySeparated α] [inst_2 : MeasurableSpace γ] [StandardBorelSpace γ],
  MeasurableSet s → Measurable f → Set.InjOn f s → MeasurableSet (f '' s)

The Lusin-Souslin theorem: if s is Borel-measurable in a standard Borel space, then its image under a measurable injective map taking values in a countably separate measurable space is also Borel-measurable.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace.CountablySeparatedMeasurableSpaceStandardBorelSpace