aedisjoint_compl_left

Mathlib.MeasureTheory.Measure.AEDisjoint

URI: https://scilib.ai/kg/mathlib#MeasureTheory.aedisjoint_compl_left

English

The complement of a set is almost everywhere disjoint from the set itself: s^c is aedisjoint from s.

Русский

Дополнение множества почти полностью несовместимо с самим множеством: s^c ⟂ s a.e.

LaTeX

$$$\\\\operatorname{AEDisjoint} \\\\mu s^c \\\\; s$$$

Lean4

theorem aedisjoint_compl_left : AEDisjoint μ sᶜ s :=
  (@disjoint_compl_left _ _ s).aedisjoint

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

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

Разделы

Аффилиация

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