integrable_indicator

Mathlib.MeasureTheory.Integral.IntegrableOn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IntegrableOn.integrable_indicator

English

If f is integrable on s, and s is measurable, then the indicator times f is integrable on μ.

Русский

Если f интегрируем на s и s измеримо, то.indicator s f интегрируем по μ.

LaTeX

$$IntegrableOn f s μ → MeasurableSet s → Integrable (indicator s f) μ$$

Lean4

theorem integrable_indicator (h : IntegrableOn f s μ) (hs : MeasurableSet s) : Integrable (indicator s f) μ :=
  (integrable_indicator_iff hs).2 h

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

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

Разделы

Аффилиация

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