ae — Mathlib · SciLib

English

If h is quasi-preserving, then for any predicate p, p almost surely on μb implies p∘f almost surely on μa.

Русский

Если h квази-сохраняет, то для любого предиката p, если p верно почти всюду в μb, то p(f(x)) верно почти всюду в μa.

LaTeX

$$ae (h) {p} (hg : ∀ᵐ x ∂μb, p x) : ∀ᵐ x ∂μa, p (f x)$$

Lean4

theorem ae (h : QuasiMeasurePreserving f μa μb) {p : β → Prop} (hg : ∀ᵐ x ∂μb, p x) : ∀ᵐ x ∂μa, p (f x) :=
  h.tendsto_ae hg

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