restrict — Mathlib

English

If f is almost everywhere measurable with respect to μ, then for any set s, f is almost everywhere μ-restricted to s-measurable.

Русский

Если f а.е.-измеримая относительно μ, то для любого множества s функция f относительно меры μ, ограниченной на s, также является а.е.-измеримой.

LaTeX

$$$AEMeasurable\ f\ \mu \rightarrow \forall s,\ AEMeasurable\ f\ (\mu.restrict\ s)$$$

Lean4

theorem restrict (hfm : AEMeasurable f μ) {s} : AEMeasurable f (μ.restrict s) :=
  ⟨AEMeasurable.mk f hfm, hfm.measurable_mk, ae_restrict_of_ae hfm.ae_eq_mk⟩

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