length_eq — Mathlib

English

The length of a Hamiltonian path equals (number of vertices) minus 1.

Русский

Длина гамильтонова пути равна количеству вершин минус 1.

LaTeX

$$$$\text{length}(p) = |V(G)| - 1.$$$$

Lean4

/-- The length of a Hamiltonian path is one less than the number of vertices of the graph. -/
theorem length_eq (hp : p.IsHamiltonian) : p.length = Fintype.card α - 1 :=
  eq_tsub_of_add_eq <| by
    rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _, ← card_eq_sum_ones,
      hp.support_toFinset, card_univ]

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