sum_of_isEmpty

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.sum_of_isEmpty

← MathLib Explorer

English

If the index type is empty, the sum is the zero measure.

Русский

Если индекс пуст, сумма равна нулевой мере.

LaTeX

$$$ [IsEmpty ι] \; (\sum μ) = 0 $$$

Lean4

@[simp]
theorem sum_of_isEmpty [IsEmpty ι] (μ : ι → Measure α) : sum μ = 0 := by
  rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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