cycleGraph_degree_two_le — Mathlib

English

In the cycle graph on n+2 vertices, the degree of any vertex v equals the cardinality of {v-1, v+1} (in particular, deg(v) = 2).

Русский

В графе цикла на n+2 вершинах степень любой вершины v равна мощности множества {v−1, v+1} (то есть deg(v) = 2).

LaTeX

$$$ (cycleGraph\ (n + 2)).degree\ v = \#\{v - 1, v + 1\} $$$

Lean4

theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
    (cycleGraph (n + 2)).degree v = Finset.card {v - 1, v + 1} := by rw [SimpleGraph.degree, cycleGraph_neighborFinset]

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