support_add

Mathlib.MeasureTheory.Measure.Support

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

← MathLib Explorer

English

The support of the sum of two measures is the union of their supports.

Русский

Опора суммы двух мер равна объединению их опор.

LaTeX

$$\\mathrm{supp}(\\mu + \\nu) = \\mathrm{supp}(\\mu) \\cup \\mathrm{supp}(\\nu)$$

Lean4

/-- The support of the sum of two measures is the union of the supports. -/
theorem support_add (μ ν : Measure X) : (μ + ν).support = μ.support ∪ ν.support := by ext; simp [mem_support_iff]

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

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

Разделы

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

Аффилиация

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