indicator_ae_eq_restrict_compl

Mathlib.MeasureTheory.Measure.Restrict

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

← MathLib Explorer

English

If s is measurable, then indicator s f is ae-equal to 0 under μ|_s^c.

Русский

Если s измеримо, индикатор s f равен 0 почти всей по μ|_{s^c}.

LaTeX

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

Lean4

theorem indicator_ae_eq_restrict_compl (hs : MeasurableSet s) : indicator s f =ᵐ[μ.restrict sᶜ] 0 := by
  classical exact piecewise_ae_eq_restrict_compl hs

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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