measure_diff_null'

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_diff_null'

English

If μ(s1 ∩ s2) = 0, then μ(s1 \\ s2) = μ(s1).

Русский

Если μ(с1 ∩ с2) = 0, тогда μ(с1 \\ с2) = μ(с1).

LaTeX

$$$$ \\mu\\left(s_{1} \\setminus s_{2}\\right) = \\mu(s_{1}) \\quad\\text{if } \\mu(s_{1} \\cap s_{2}) = 0. $$$$

Lean4

theorem measure_diff_null' (h : μ (s₁ ∩ s₂) = 0) : μ (s₁ \ s₂) = μ s₁ :=
  measure_congr <| diff_ae_eq_self.2 h

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

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

Разделы

Аффилиация

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