of_diff

Mathlib.MeasureTheory.VectorMeasure.Basic

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

← MathLib Explorer

English

If A ⊆ B, then v(B \\ A) = v(B) − v(A).

Русский

Если A ⊆ B, то v(B \\ A) = v(B) − v(A).

LaTeX

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

Lean4

theorem of_diff {M : Type*} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {v : VectorMeasure α M} {A B : Set α}
    (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : v (B \ A) = v B - v A := by
  rw [← of_add_of_diff hA hB h, add_sub_cancel_left]

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

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

Разделы

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

Аффилиация

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