preimage — Mathlib

English

For a quasi-measure-preserving f, given a null-measurable set s and hs' : f^{-1} s =ᵐ s, there exists t with t measurable, t =ᵐ s, and f^{-1} t = t.

Русский

Для f с квазимерующим свойством существует измеримое t, эквивалентное s почти по μ и инвариантное относительно f.

LaTeX

$$∃ t, MeasurableSet t ∧ t =_{ae}^{μ} s ∧ f^{-1}(t) = t$$

Lean4

theorem preimage {ν : Measure β} {f : α → β} {s t : Set β} (ht : AEDisjoint ν s t) (hf : QuasiMeasurePreserving f μ ν) :
    AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t) :=
  hf.preimage_null ht

Похожие утверждения