measure_diff_left

Mathlib.MeasureTheory.Measure.AEDisjoint

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

English

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

Русский

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

LaTeX

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

Lean4

theorem measure_diff_left (h : AEDisjoint μ s t) : μ (s \ t) = μ s :=
  measure_congr <| AEDisjoint.diff_ae_eq_left h

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

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

Разделы

Аффилиация

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