aemeasurable_of_map_neZero — Mathlib

English

If the pushforward measure μ.map f is nonzero, then f is AEMeasurable with respect to μ.

Русский

Если образная мера μ.map f не нулевая, то f является AEMeasurable относительно μ.

LaTeX

$$$\\\\text{NeZero}(\\\\mu\\\\map f) \\\\Rightarrow \\\\text{AEMeasurable}(f,\\\\mu)$$$

Lean4

theorem aemeasurable_of_map_neZero {μ : Measure α} {f : α → β} (h : NeZero (μ.map f)) : AEMeasurable f μ :=
  by
  by_contra h'
  simp [h'] at h

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