measure_diff_right

Mathlib.MeasureTheory.Measure.AEDisjoint

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEDisjoint.measure_diff_right

English

If s and t are μ-a.e. disjoint, then μ(t \\ s) = μ(t).

Русский

Если s и t по μ почти не пересекаются, то μ(t \ s) = μ(t).

LaTeX

$$$\\\\mu (t \\\\setminus s) = \\\\mu(t)$$$

Lean4

theorem measure_diff_right (h : AEDisjoint μ s t) : μ (t \ s) = μ t :=
  measure_congr <| AEDisjoint.diff_ae_eq_right h

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

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

Разделы

Аффилиация

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