exists_isTree_le — Mathlib

English

Every connected graph has a spanning tree.

Русский

Каждый связный граф имеет растяжённое дерево ( spanning tree ).

LaTeX

$$$[Finite\ V] (G.Connected) \Rightarrow \exists T \le G, IsTree\ T$$$

Lean4

/-- Every connected graph has a spanning tree. -/
theorem exists_isTree_le [Finite V] (h : G.Connected) : ∃ T ≤ G, IsTree T :=
  by
  obtain ⟨T, hTG, hmin⟩ := {H : SimpleGraph V | H.Connected}.toFinite.exists_le_minimal h
  exact ⟨T, hTG, isTree_of_minimal_connected hmin⟩

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