length_eq — Mathlib

English

For a finite vertex set, the length of a Hamiltonian cycle equals the number of vertices: p.length = card α.

Русский

Для конечного множества вершин длина гамильтонова цикла равна числу вершин: p.length = card α.

LaTeX

$$$p.IsHamiltonianCycle \rightarrow p.length = Fintype.card α$$$

Lean4

/-- The length of a Hamiltonian cycle is the number of vertices. -/
theorem length_eq [Fintype α] (hp : p.IsHamiltonianCycle) : p.length = Fintype.card α :=
  by
  rw [← length_tail_add_one hp.not_nil, hp.isHamiltonian_tail.length_eq, Nat.sub_add_cancel]
  rw [Nat.succ_le, Fintype.card_pos_iff]
  exact ⟨a⟩

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