partOfVertex_mem

Mathlib.Combinatorics.SimpleGraph.Partition

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

English

For any vertex v, the vertex v belongs to its partition block, i.e., v ∈ P.partOfVertex v.

Русский

Для любой вершины v верно, что v принадлежит своему блоку разбиения: v ∈ P.partOfVertex v.

LaTeX

$$$v \\in P.partOfVertex(v)$$$

Lean4

theorem partOfVertex_mem (v : V) : P.partOfVertex v ∈ P.parts :=
  by
  obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1
  exact h

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

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

Разделы

Аффилиация

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