lintegral_zero_measure

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

For any f, the lintegral with respect to the zero measure is 0: ∫ f d0 = 0.

Русский

Для любой функции f линегральный интеграл по нулевой мере равен нулю: ∫ f d0 = 0.

LaTeX

$$$\\int f \\, d(0: Measure \\alpha) = 0$$$

Lean4

@[simp]
theorem lintegral_zero_measure {m : MeasurableSpace α} (f : α → ℝ≥0∞) : ∫⁻ a, f a ∂(0 : Measure α) = 0 := by
  simp [lintegral]

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

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

Разделы

Аффилиация

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