isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one

English

A Hamiltonian cycle induces a cycle whose tail contains each vertex exactly once.

Русский

Гамильтонов цикл порождает цикл, хвост которого содержит каждую вершину ровно по одному разу.

LaTeX

$$$$p.IsHamiltonianCycle \Rightarrow p.IsCycle \land \forall a, (p.tail).count(a) = 1.$$$$

Lean4

theorem isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one :
    p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ a, (support p).tail.count a = 1 := by
  simp +contextual [isHamiltonianCycle_isCycle_and_isHamiltonian_tail, IsHamiltonian, support_tail, IsCycle.not_nil]

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