indicator

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#Measurable.indicator

← MathLib Explorer

English

If f is measurable and s is a measurable set, then s.indicator f is measurable.

Русский

Если f измерима и s измеримо, то s.indicator f измерима.

LaTeX

$$$\\text{Measurable } f \\to \\text{MeasurableSet } s \\to \\text{Measurable } (s.indicator f)$$$

Lean4

@[measurability, fun_prop]
theorem indicator [Zero β] (hf : Measurable f) (hs : MeasurableSet s) : Measurable (s.indicator f) :=
  hf.piecewise hs measurable_const

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

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

Разделы

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

Аффилиация

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