of_add_of_diff

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.of_add_of_diff

← MathLib Explorer

English

If A ⊆ B and A, B are measurable, then v(A) + v(B \\ A) = v(B).

Русский

Если A ⊆ B и A, B измеримы, то v(A) + v(B \\ A) = v(B).

LaTeX

$$v A + v (B \\ A) = v B$$

Lean4

theorem of_add_of_diff {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) :
    v A + v (B \ A) = v B := by
  rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]

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

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

Разделы

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

Аффилиация

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