theorem Graph.Connected.isTree_of_maximal_isAcyclicSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hG : G.Connected) (hF : Maximal G.IsAcyclicSet F) : (G.restrict F).IsTree

If G is connected, then a maximally acylic subgraph of G is connected. The correct statement is that any two vertices connected in the big graph are connected in the small one.

theorem Graph.Connected.exists_isTree_spanningSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : ∃ (T : Graph α β), T.IsTree ∧ T ≤s G

Every connected graph has a spanning tree

theorem Graph.Connected.encard_vertexSet_le {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Connected) : G.vertexSet.encard ≤ G.edgeSet.encard + 1

theorem Graph.Connected.ncard_vertexSet_le {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.Connected) : G.vertexSet.ncard ≤ G.edgeSet.ncard + 1