count_support_self — Mathlib

English

In a Hamiltonian cycle p on G starting and ending at a, the start vertex a appears exactly twice in the vertex list; any other vertex appears exactly once.

Русский

В гамильтонова цикле p вершина a встречается дважды, все остальные вершины — один раз.

LaTeX

$$$p.IsHamiltonianCycle \rightarrow p.support.count a = 2$$$

Lean4

theorem count_support_self (hp : p.IsHamiltonianCycle) : p.support.count a = 2 := by
  rw [support_eq_cons, List.count_cons_self, ← support_tail _ hp.1.not_nil, hp.isHamiltonian_tail]

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