setLIntegral_empty

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

For any f, ∫ over the empty set is 0: ∫⁻ x in ∅, f x ∂μ = 0.

Русский

Для любого f интеграл по пустому множеству равен нулю.

LaTeX

$$$\\int⁻ x in \\emptyset, f x \\, d\\mu = 0$$$

Lean4

theorem setLIntegral_empty (f : α → ℝ≥0∞) : ∫⁻ x in ∅, f x ∂μ = 0 := by
  rw [Measure.restrict_empty, lintegral_zero_measure]

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

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

Разделы

Аффилиация

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