tendsto_ae_map — Mathlib

English

Mapping a.e.-convergent sequence preserves almost everywhere convergence of images: Tendsto f from ae μ to ae (μ.map f).

Русский

Переход по a.e. сходящимся последовательностям сохраняет сходимость почти повсюду в образах.

LaTeX

$$$ \text{tendsto } f\, (\mathrm{ae}\, \mu) \; (\mathrm{ae}\, (\mathrm{map}\ f\ \mu)) $$$

Lean4

theorem tendsto_ae_map {f : α → β} (hf : AEMeasurable f μ) : Tendsto f (ae μ) (ae (μ.map f)) := fun _ hs =>
  preimage_null_of_map_null hf hs

Похожие утверждения