mono

Mathlib.Combinatorics.SimpleGraph.Hamiltonian

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

← MathLib Explorer

English

If G ≤ H and G is Hamiltonian, then H is Hamiltonian.

Русский

Если G является подграфом H и G гамильтониан, тогда H гамильтониан.

LaTeX

$$$G \le H \rightarrow (G.IsHamiltonian) \rightarrow H.IsHamiltonian$$$

Lean4

theorem mono {H : SimpleGraph α} (hGH : G ≤ H) (hG : G.IsHamiltonian) : H.IsHamiltonian := fun hα ↦
  let ⟨_, p, hp⟩ := hG hα;
  ⟨_, p.map <| .ofLE hGH, hp.map _ bijective_id⟩

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

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

Разделы

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

Аффилиация

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