of_map_ne_zero — Mathlib

English

If f =ᵐ[μ] g, then μ.map f = μ.map g.

Русский

Если f и g совпадают почти повсеместно относительно μ, то их образы по μ совпадают: μ.map f = μ.map g.

LaTeX

$$$ f =_{\mathrm{ae}}^{\mu} g \Rightarrow \mu.map f = \mu.map g $$$

Lean4

theorem _root_.AEMeasurable.of_map_ne_zero {f : α → β} {μ : Measure α} (hf : μ.map f ≠ 0) : AEMeasurable f μ :=
  not_imp_comm.1 map_of_not_aemeasurable hf

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