mem_partOfVertex

Mathlib.Combinatorics.SimpleGraph.Partition

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

English

For vertex v, the set P.partOfVertex v is a member of P.parts.

Русский

Для вершины v множество P.partOfVertex v является элементом разбиения P.

LaTeX

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

Lean4

theorem mem_partOfVertex (v : V) : v ∈ P.partOfVertex v :=
  by
  obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec
  exact h

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

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

Разделы

Аффилиация

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