partOfVertex

Mathlib.Combinatorics.SimpleGraph.Partition

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Partition.partOfVertex

English

The part in the partition that a vertex v belongs to is the block containing v.

Русский

Часть разбиения, в которую попадает вершина v, есть блок, содержащий v.

LaTeX

$$$P.partOfVertex(v)$$$

Lean4

/-- The part in the partition that `v` belongs to -/
def partOfVertex (v : V) : Set V :=
  Classical.choose (P.isPartition.2 v)

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

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

Разделы

Аффилиация

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