preimage_ae_eq — Mathlib

English

Let f be quasi-measure-preserving from μa to μb. If s and t are almost everywhere equal with respect to μb, then their preimages are almost everywhere equal with respect to μa.

Русский

Пусть f — квазимерущее отображение между μa и μb. Если множества s и t равны почти всюду по μb, то их предобраза равны почти всюду по μa.

LaTeX

$$$f^{-1}(s) =_{ae}^{\mu_a} f^{-1}(t)$$$

Lean4

theorem preimage_ae_eq {s t : Set β} (hf : QuasiMeasurePreserving f μa μb) (h : s =ᵐ[μb] t) : f ⁻¹' s =ᵐ[μa] f ⁻¹' t :=
  EventuallyLE.antisymm (hf.preimage_mono_ae h.le) (hf.preimage_mono_ae h.symm.le)

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