Theorems · Theorem · measure theory

MeasureTheory.isClosed_setOfPred_preimage_ae_eq

∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X]
  [R1Space X] [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
  [inst_8 : TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)},
  Continuous f →
    (∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) →
      ∀ (s : Set X) {t : Set Y}, MeasureTheory.NullMeasurableSet t ν → ν t ≠ ⊤ → IsClosed {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}

Let f : Z → C(X, Y) be a continuous (in the compact open topology) family of continuous measure-preserving maps. Let t : Set Y be a null measurable set of finite measure. Then for any s, the set of parameters z such that the preimage of t under f_z is a.e. equal to s is a closed set. In particular, if X = Y and s = t, then we see that the a.e. stabilizer of a set is a closed set.

Defined in

Mathlib.MeasureTheory.Measure.ContinuousPreimage

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceTopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceTopologicalSpaceMeasureTheory.Measure.InnerRegularCompactLTTopMeasureTheory.IsLocallyFiniteMeasure