AEDisjoint

Mathlib.MeasureTheory.Measure.AEDisjoint

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

English

Two sets are μ-almost everywhere disjoint if their intersection has measure zero.

Русский

Множества μ-почти попарно не пересекаются, если их пересечение имеет меру ноль.

LaTeX

$$$\text{AEDisjoint }(s,t) := μ(s \cap t) = 0$$$

Lean4

/-- Two sets are said to be `μ`-a.e. disjoint if their intersection has measure zero. -/
def AEDisjoint (s t : Set α) :=
  μ (s ∩ t) = 0

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

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

Разделы

Аффилиация

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