structure Graph.IsTree {α : Type u_1} {β : Type u_2} (T : Graph α β) : Prop

• isForest : T.IsForest
• connected : T.Connected

theorem Graph.isTree_iff {α : Type u_1} {β : Type u_2} (T : Graph α β) : T.IsTree ↔ T.IsForest ∧ T.Connected

theorem Graph.IsForest.isTree_of_IsCompOf {α : Type u_1} {β : Type u_2} {G T : Graph α β} (hG : G.IsForest) (hT : T.IsCompOf G) : T.IsTree

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.edgeRestrict 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. TODO : Write the proof completely in terms of IsAcyclicSet

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.IsTree.exists_delete_vertex_isTree {α : Type u_1} {β : Type u_2} {T : Graph α β} [T.Finite] (hT : T.IsTree) (hnt : T.vertexSet.Nontrivial) : ∃ v ∈ T.vertexSet, (T - {v}).IsTree

theorem Graph.IsLeaf.delete_isTree {α : Type u_1} {β : Type u_2} {T : Graph α β} {x : α} (hT : T.IsTree) (hx : T.IsLeaf x) : (T - {x}).IsTree

@[irreducible]

theorem Graph.IsTree.encard_vertexSet {α : Type u_1} {β : Type u_2} {T : Graph α β} (h : T.IsTree) : T.vertexSet.encard = T.edgeSet.encard + 1

theorem Graph.IsTree.ncard_vertexSet {α : Type u_1} {β : Type u_2} {T : Graph α β} [T.Finite] (h : T.IsTree) : T.vertexSet.ncard = T.edgeSet.ncard + 1

theorem Graph.IsForest.encard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) : G.vertexSet.encard = G.edgeSet.encard + {C : Graph α β | C.IsCompOf G}.encard

theorem Graph.IsForest.ncard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.IsForest) : G.vertexSet.ncard = G.edgeSet.ncard + {C : Graph α β | C.IsCompOf G}.ncard

theorem Graph.IsForest.encard_edgeSet_add_one_le {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) (hne : G.vertexSet.Nonempty) : G.edgeSet.encard + 1 ≤ G.vertexSet.encard

theorem Graph.IsForest.ncard_edgeSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.IsForest) (hne : G.vertexSet.Nonempty) : G.edgeSet.ncard < G.vertexSet.ncard

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