disjoint

Mathlib.Data.Setoid.Partition

URI: https://scilib.ai/kg/mathlib#IndexedPartition.disjoint

English

The blocks s_i are pairwise disjoint.

Русский

Блоки s_i попарно не пересекаются.

LaTeX

$$$\\\\forall i \\\\neq j,\\ s_i \\cap s_j = \\\\emptyset$$$

Lean4

theorem disjoint : Pairwise (Disjoint on s) := fun {_i _j} h =>
  disjoint_left.mpr fun {_x} hxi hxj => h (hs.eq_of_mem hxi hxj)

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

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

Разделы

Аффилиация

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