isPath

Mathlib.Combinatorics.SimpleGraph.Hamiltonian

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.IsHamiltonian.isPath

← MathLib Explorer

English

Hamiltonian paths are paths.

Русский

Гамильтоновы пути являются путями.

LaTeX

$$$$\text{IsHamiltonian}(p) \Rightarrow \text{IsPath}(p).$$$$

Lean4

/-- Hamiltonian paths are paths. -/
theorem isPath (hp : p.IsHamiltonian) : p.IsPath :=
  IsPath.mk' <| List.nodup_iff_count_le_one.2 <| (le_of_eq <| hp ·)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru