mono_ac — Mathlib

English

If f is AEMeasurable with respect to ν and μ ≪ ν, then f is AEMeasurable with respect to μ.

Русский

Если f — μ-важное AEMeasurable относительно ν и μ абсолютно непрерывна по ν, то f — μ-AEMeasurable.

LaTeX

$$$\\\\text{AEMeasurable}(f,\\\\nu) \\\\land \\\\mu \\\\\\ll \\\\nu \\\Rightarrow \\\\text{AEMeasurable}(f,\\\\mu)$$$

Lean4

theorem mono_ac (hf : AEMeasurable f ν) (hμν : μ ≪ ν) : AEMeasurable f μ :=
  ⟨hf.mk f, hf.measurable_mk, hμν.ae_le hf.ae_eq_mk⟩

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