ae_restrict_iff_subtype — Mathlib

English

Equivalence between almost everywhere statements on μ.restrict s and on comap by Subtype.val, for measurable s.

Русский

Эквивалентность утверждений почти всюду относительно μ|_s и относительно comap по Subtype.val для измеримого s.

LaTeX

$$$\forall p,\; (\forall^{\mathrm{ae}} x \partial μ.restrict s, p x) \iff (\forall^{\mathrm{ae}} x \partial \mathrm{comap}(\mathrm{Subtype.val}, μ), p x).$$$

Lean4

theorem ae_restrict_iff_subtype {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s)
    {p : α → Prop} : (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ (x : s) ∂comap ((↑) : s → α) μ, p x := by
  rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]

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