mono' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
protected theorem mono' (h : AEMeasurable f μ) (h' : ν ≪ μ) : AEMeasurable f ν :=
  ⟨h.mk f, h.measurable_mk, h' h.ae_eq_mk⟩

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