pairwiseDisjoint

Mathlib.Order.Partition.Basic

URI: https://scilib.ai/kg/mathlib#Partition.pairwiseDisjoint

English

The blocks of a partition form a pairwise disjoint family.

Русский

Блоки разбиения образуют пару взаимно непересекающихся элементов.

LaTeX

$$Set.PairwiseDisjoint (P : Set α) id$$

Lean4

theorem pairwiseDisjoint : Set.PairwiseDisjoint (P : Set α) id :=
  P.sSupIndep'.pairwiseDisjoint

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

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

Разделы

Аффилиация

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