isHamiltonianCycle_isCycle_and_isHamiltonian_tail

English

A Hamiltonian cycle p is equivalent to p being a cycle and its tail support has count 1 for every vertex.

Русский

Гамильтонов цикл p эквивалентен тому, что p является циклом и для каждого вершины в хвосте p.tail количество вхождений равно 1.

LaTeX

$$$$p.IsHamiltonianCycle \iff p.IsCycle \land \forall a, (\text{support } p).tail.count(a) = 1.$$$$

Lean4

theorem isHamiltonianCycle_isCycle_and_isHamiltonian_tail : p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.tail.IsHamiltonian :=
  ⟨fun ⟨h, h'⟩ ↦ ⟨h, h'⟩, fun ⟨h, h'⟩ ↦ ⟨h, h'⟩⟩

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