indicator_ae_eq_restrict

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#indicator_ae_eq_restrict

English

If s is measurable, indicator s f is ae-equal to f with respect to the restricted measure μ|_s.

Русский

Если s измеримо, то индикатор s f равен a.e. f относительно μ|_s.

LaTeX

$$$ \\text{indicator } s\\, f =_{\\mathrm{ae}}^{\\mu|_s} f $$$

Lean4

theorem indicator_ae_eq_restrict (hs : MeasurableSet s) : indicator s f =ᵐ[μ.restrict s] f := by
  classical exact piecewise_ae_eq_restrict hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru