cycleGraph_degree_three_le — Mathlib

English

In the cycle graph on n+3 vertices, every vertex has degree 2.

Русский

В графе цикла на n+3 вершинах каждая вершина имеет степень 2.

LaTeX

$$$ (cycleGraph\ (n + 3)).degree\ v = 2 $$$

Lean4

theorem cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} : (cycleGraph (n + 3)).degree v = 2 :=
  by
  rw [cycleGraph_degree_two_le, Finset.card_pair]
  simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]
  exact ne_of_beq_false rfl

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