aedisjoint_compl_right

Mathlib.MeasureTheory.Measure.AEDisjoint

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

English

The set s is μ-a.e. disjoint from its complement: s is aedisjoint from s^c.

Русский

Множество s почти не пересекается с своим дополнением: s ⟂ s^c по μ.

LaTeX

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

Lean4

theorem aedisjoint_compl_right : AEDisjoint μ s sᶜ :=
  (@disjoint_compl_right _ _ s).aedisjoint

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

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

Разделы

Аффилиация

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