mono_measure — Mathlib

English

If f is AEMeasurable w.r.t. μ and ν ≤ μ, then f is AEMeasurable w.r.t. ν.

Русский

Если f измеримо почти всюду относительно μ и ν ≤ μ, то f измеримо почти всюду относительно ν.

LaTeX

$$$$ AEMeasurable(f,\\mu) \\land \\nu \\le \\mu \\Rightarrow AEMeasurable(f,\\nu). $$$$

Lean4

theorem mono_measure (h : AEMeasurable f μ) (h' : ν ≤ μ) : AEMeasurable f ν :=
  mono_ac h h'.absolutelyContinuous

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