English
For measurable s and μ, restricting to s commutes with passing to the subtype comap, yielding a relation between almost everywhere statements on the subtype and on μ.
Русский
Для измеримого s и μ ограничение и переход к подтипу комап взаимно согласованы: утверждения почти всюду на подтипе соответствуют почти всюду относительно μ.
LaTeX
$$$\\text{ae}_{\\mu|_s} (p) \\leftrightarrow \\text{ae}_{\\mathrm{comap}\\; (\\mathrm{incl})\, μ} (p)$$$
Lean4
theorem comap_apply (μ : Measure β) (s : Set α) : comap f μ s = μ (f '' s) :=
calc
comap f μ s = comap f μ (f ⁻¹' (f '' s)) := by rw [hf.injective.preimage_image]
_ = (comap f μ).map f (f '' s) := (hf.map_apply _ _).symm
_ = μ (f '' s) := by
rw [hf.map_comap, restrict_apply' hf.measurableSet_range, inter_eq_self_of_subset_left (image_subset_range _ _)]
