nullMeasurable — Mathlib

English

If a function f is almost everywhere measurable with respect to μ, then f is NullMeasurable with respect to μ.

Русский

Если функция f измерима почти всюду по отношению к μ, то она нулевомерна по μ.

LaTeX

$$AEMeasurable f μ → NullMeasurable f μ$$

Lean4

protected theorem _root_.AEMeasurable.nullMeasurable {f : α → β} (h : AEMeasurable f μ) : NullMeasurable f μ :=
  let ⟨_g, hgm, hg⟩ := h;
  hgm.nullMeasurable.congr hg.symm

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