integrableOn_zero

Mathlib.MeasureTheory.Integral.IntegrableOn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.integrableOn_zero

English

The statement that the zero function is integrable on any set is a base simplification.

Русский

Утверждение, что нулевая функция интегрируема на любом множестве, является базовым упрощением.

LaTeX

$$$ \text{IntegrableOn}(0, s, \mu) $$$

Lean4

theorem integrableOn_zero : IntegrableOn (fun _ => (0 : ε')) s μ :=
  integrable_zero _ _ _

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

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

Разделы

Аффилиация

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