English
If s is NullMeasurable with respect to comap f μ, then f''s is NullMeasurable with respect to μ, under the injected f and the null-measurability condition.
Русский
Если s нуль-мезируемо относительно comap f μ, то f''s тоже нуль-мезируемо относительно μ при условии инъективности и соответственно.
LaTeX
$$NullMeasurableSet(s) (comap f μ) → NullMeasurableSet(f''s) μ$$
Lean4
theorem image (f : α → β) (μ : Measure β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ)
(hs : NullMeasurableSet s (μ.comap f)) : NullMeasurableSet (f '' s) μ :=
by
refine ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, ?_⟩
refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm
swap
· exact hf _ (measurableSet_toMeasurable _ _)
have h : toMeasurable (comap f μ) s =ᵐ[comap f μ] s := NullMeasurableSet.toMeasurable_ae_eq hs
exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm
