Theorems · Theorem · general topology

Measurable.measurableSet_preimage_iff_inter_range

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

If f : X → Z is a Borel measurable map from a standard Borel space to a countably separated measurable space and the range of f is measurable, then the preimage of a set s is measurable if and only if the intersection with Set.range f is measurable.

Defined in

Mathlib.MeasureTheory.Constructions.Polish.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceMeasurableSpaceMeasurableSpace.CountablySeparated