English
Let f: α → β be a function and assume range f is measurable. Then almost every x with respect to μ.map f lies in the range of f.
Русский
Пусть f: α → β — функция, и множество range f измеримо. Тогда почти наверняка по μ,map f точки лежат в range f.
LaTeX
$$$$\\forall m_0:\\text{MeasurableSpace } \\alpha\\; (f:\\alpha\\to \\beta),\\; \\mathrm{MeasurableSet}(\\mathrm{range}(f))\\; (\\mu:\\mathrm{Measure}\\,\\alpha) : \\forall^{\\mathrm{ae}} x\\; \\partial(\\mu.map f),\\; x \\in \\mathrm{range}(f).$$$$
Lean4
theorem ae_map_mem_range {m0 : MeasurableSpace α} (f : α → β) (hf : MeasurableSet (range f)) (μ : Measure α) :
∀ᵐ x ∂μ.map f, x ∈ range f := by
by_cases h : AEMeasurable f μ
· change range f ∈ ae (μ.map f)
rw [mem_ae_map_iff h hf]
filter_upwards using mem_range_self
· simp [map_of_not_aemeasurable h]
