ae_map_iff_ae_trim — Mathlib

English

Let f be measurable and hp is measurable set; then almost everywhere property under μ.map f is equivalent to the corresponding property under μ.trim by f.

Русский

Пусть f измеримо, и hp — измеримое множество. Тогда свойство почти всюду относительно μ.map f эквивалентно соответствующему свойству относительно μ.trim через f.

LaTeX

$$$(\\forall p,\\, p\\text{ measurable},\\; p\\text{ holds a.e. under } μ.map f) \\iff (p\\circ f) \\text{ holds a.e. under } μ.trim hm.$$$

Lean4

theorem ae_map_iff_ae_trim {f : α → β} (hf : Measurable f) {p : β → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ y ∂μ.map f, p y) ↔ ∀ᵐ x ∂(μ.trim hf.comap_le), p (f x) := by
  rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]

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