integrableOn_empty

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

The zero function is integrable on the empty set with any measure.

Русский

Нулевая функция интегрируема на пустом множестве любой мере.

LaTeX

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

Lean4

@[simp]
theorem integrableOn_empty : IntegrableOn f ∅ μ := by simp [IntegrableOn]

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

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

Разделы

Аффилиация

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