Leaves of finite forests #
[UPSTREAM] candidate for Mathlib/Combinatorics/SimpleGraph/Acyclic.lean: a nonempty forest
with finitely many edges has a vertex with at most one neighbour, the forest analogue of
SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial.
theorem
SimpleGraph.IsAcyclic.exists_neighborSet_subsingleton
{V : Type u_1}
{G : SimpleGraph V}
[Nonempty V]
[Finite ↑G.edgeSet]
(hG : G.IsAcyclic)
:
∃ (v : V), (G.neighborSet v).Subsingleton