IsRegularOfDegree — Mathlib

English

Definition: A locally finite simple graph G is regular of degree d if every vertex has degree d.

Русский

Определение: локально конечный простой граф G — регулярный степени d, если каждая вершина имеет степень d.

LaTeX

$$G.IsRegularOfDegree d ⇔ ∀ v, deg_G(v) = d$$

Lean4

/-- A locally finite simple graph is regular of degree `d` if every vertex has degree `d`. -/
def IsRegularOfDegree (d : ℕ) : Prop :=
  ∀ v : V, G.degree v = d

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