top

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsRegularOfDegree.top

English

The top graph is regular of degree |V| - 1.

Русский

Верхний граф является регулярным степени |V| - 1.

LaTeX

$$∀ v, deg_{\top}(v) = |V| - 1$$

Lean4

theorem top [DecidableEq V] : (⊤ : SimpleGraph V).IsRegularOfDegree (Fintype.card V - 1) :=
  by
  intro v
  simp

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

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

Разделы

Аффилиация

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