English
Let f: α → β be almost everywhere measurable with respect to μ. If a property p on β holds almost everywhere with respect to the pushforward measure μ.map f, then p(f(x)) holds almost everywhere with respect to μ on α.
Русский
Пусть f: α → β почти всюду измерима относительно μ. Если свойство p на β выполняется почти всюду относительно меры μ.map f, то p(f(x)) выполняется почти всюду относительно μ на α.
LaTeX
$$$$\\forall f: \\alpha \\to \\beta,\\; \\mathrm{AEMeasurable}(f,\\mu) \\rightarrow \\Big(\\forall p: \\beta \\to \\mathrm{Prop},\\; \\forall^{\\mathrm{ae}} y\\; \\partial(\\mu.map f),\\; p(y) \\Big) \\\\rightarrow \\, \\forall^{\\mathrm{ae}} x\\; \\partial\\mu,\\; p(f(x)).$$$$
Lean4
theorem ae_of_ae_map {f : α → β} (hf : AEMeasurable f μ) {p : β → Prop} (h : ∀ᵐ y ∂μ.map f, p y) : ∀ᵐ x ∂μ, p (f x) :=
mem_ae_of_mem_ae_map hf h
