Theorems · Theorem · general topology

Measurable.measurableSet_preimage_iff_of_surjective

∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s

If f : X → Z is a surjective Borel measurable map from a standard Borel space to a countably separated measurable space, then the preimage of a set s is measurable if and only if the set is measurable. One implication is the definition of measurability, the other one heavily relies on X being a standard Borel space.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceMeasurableSpaceMeasurableSpace.CountablySeparated