support_count_of_ne — Mathlib

English

If p is a Hamiltonian cycle and a ≠ b, then b occurs exactly once in p.support.

Русский

Если p — гамильтонов цикл и a ≠ b, то вершина b встречается в p.support ровно один раз.

LaTeX

$$$p.IsHamiltonianCycle \rightarrow a \neq b \rightarrow p.support.count b = 1$$$

Lean4

theorem support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a ≠ b) : p.support.count b = 1 := by
  rw [← cons_support_tail p hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]

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