connected — Mathlib

English

If a graph is Hamiltonian, then it is connected.

Русский

Если граф гамильтониан, то он связный.

LaTeX

$$$G.IsHamiltonian \rightarrow G.Connected$$$

Lean4

theorem connected (hG : G.IsHamiltonian) : G.Connected
    where
  preconnected a
    b := by
    obtain rfl | hab := eq_or_ne a b
    · rfl
    have : Nontrivial α := ⟨a, b, hab⟩
    obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'
    have a_mem := hp.mem_support a
    have b_mem := hp.mem_support b
    exact ((p.takeUntil a a_mem).reverse.append <| p.takeUntil b b_mem).reachable
  nonempty := not_isEmpty_iff.1 fun _ ↦ by simpa using hG <| by simp [@Fintype.card_eq_zero]

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