ae_map_iff — Mathlib

English

If s is measurable, then almost everywhere statements on μ.restrict s are equivalent to almost everywhere statements on comap by the subtype embedding.

Русский

Если s измеримо, то утверждения почти всюду относительно μ|_s эквивалентны утверждениям относительно comap по подтипу.

LaTeX

$$$\\text{ae}_{μ|_s}(p) \\iff \\text{ae}_{\\mathrm{comap}\\; (\\mathrm{Subtype.val})\, μ}(p).$$$

Lean4

theorem ae_map_iff {p : β → Prop} {μ : Measure α} : (∀ᵐ x ∂μ.map f, p x) ↔ ∀ᵐ x ∂μ, p (f x) := by
  simp only [ae_iff, hf.map_apply, preimage_setOf_eq]

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