ae_map_iff — Mathlib

English

For AEMeasurable f, and any predicate p with measurable set {x | p x}, (∀ᵐ y in μ.map f, p y) iff (∀ᵐ x in μ, p (f x)).

Русский

Для AEMеас measurable f и любого предиката p с измеримым множеством {x | p x}, (∀ᵐ y в μ.map f, p y) эквивалентно (∀ᵐ x в μ, p (f x)).

LaTeX

$$$ \forall f,\; \mathrm{AEMeasurable}(f, \mu) \rightarrow ( (\forall^{\ast} y \; p(y)\; \text{на } \mu.map f) \iff (\forall^{\ast} x \; p(f(x))\; \text{на } \mu) ) $$$

Lean4

theorem ae_map_iff {f : α → β} (hf : AEMeasurable f μ) {p : β → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ y ∂μ.map f, p y) ↔ ∀ᵐ x ∂μ, p (f x) :=
  mem_ae_map_iff hf hp

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