mem_support — Mathlib

English

If p is a Hamiltonian cycle of G, then every vertex of G appears on p.

Русский

Если p — гамильтонов цикл графа G, то каждая вершина графа встречается на p.

LaTeX

$$$p.IsHamiltonianCycle \rightarrow \forall b:\alpha, b \in p.support$$$

Lean4

/-- A Hamiltonian cycle visits every vertex. -/
theorem mem_support (hp : p.IsHamiltonianCycle) (b : α) : b ∈ p.support :=
  List.mem_of_mem_tail <| support_tail p hp.1.not_nil ▸ hp.isHamiltonian_tail.mem_support _

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