biUnion_parts

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.biUnion_parts

English

The union of all parts in P.parts equals s.

Русский

Объединение всех частей P.parts равно s.

LaTeX

$$$ \bigcup_{t \in P.parts} t = s $$$

Lean4

theorem biUnion_parts : P.parts.biUnion id = s :=
  (sup_eq_biUnion _ _).symm.trans P.sup_parts

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

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

Разделы

Аффилиация

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