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]