restrict — Mathlib

English

If f is AEStronglyMeasurable on μ, then restricting the measure to any set s preserves AEStronglyMeasurable.

Русский

Если f AE‑строго измерима по μ, то ограничение меры до множества s сохраняет AE‑строго измеримость.

LaTeX

$$$AEStronglyMeasurable_m(f, \\mu) \\Rightarrow AEStronglyMeasurable_m(f, \\mu.restrict s)$$$

Lean4

@[fun_prop]
protected theorem restrict (hfm : AEStronglyMeasurable[m] f μ) {s} : AEStronglyMeasurable[m] f (μ.restrict s) :=
  hfm.mono_measure Measure.restrict_le_self

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