degree

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.degree

English

The degree of v is the number of vertices adjacent to v, i.e., the size of the neighborFinset.

Русский

Степень вершины v равна числу вершин, соседних с v; то есть размеру множества neighborFinset v.

LaTeX

$$$ \text{degree} : = #( G.neighborFinset v ) $$$

Lean4

/-- `G.degree v` is the number of vertices adjacent to `v`. -/
def degree : ℕ :=
  #(G.neighborFinset v)

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

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

Разделы

Аффилиация

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