English
For an injective f with measurable-preserving property, comap f μ s equals μ(f''s) for measurable s.
Русский
Для инъективного отображения f, сохраняющего измеримые множества, верно comap f μ s = μ(f''s).
LaTeX
$$$\operatorname{comap}_l f μ(s) = μ(f''s)$$$
Lean4
/-- Pullback of a `Measure`. If `f` sends each measurable set to a null-measurable set,
then for each measurable set `s` we have `comap f μ s = μ (f '' s)`.
Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. -/
def comap [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : Measure β) : Measure α :=
if hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ then
(OuterMeasure.comap f μ.toOuterMeasure).toMeasure fun s hs t =>
by
simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]
exact (measure_inter_add_diff₀ _ (hf.2 s hs)).symm
else 0
