measure_add_diff

Mathlib.MeasureTheory.Measure.MeasureSpace

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

← MathLib Explorer

English

If s is null-measurable and t is any set, then μ(s) + μ(t \\ s) = μ(s ∪ t).

Русский

Если s нулемеримо измеримо, тогда μ(s) + μ(t \\ s) = μ(s ∪ t).

LaTeX

$$$$ \\mu(s) + \\mu(t \\setminus s) = \\mu(s \\cup t). $$$$

Lean4

theorem measure_add_diff (hs : NullMeasurableSet s μ) (t : Set α) : μ s + μ (t \ s) = μ (s ∪ t) := by
  rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_diff_self]

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

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

Разделы

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

Аффилиация

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