Neighbours of a vertex of large degree

A vertex of degree at least three keeps two distinct neighbours after any single vertex is set aside. This is the step that grows a branch vertex into a star: the vertex set aside is the neighbour already used, for instance the next vertex along a path, and the two remaining neighbours are new leaves.

Main results

• SimpleGraph.exists_adj_adj_ne_of_three_le_degree: a vertex of degree at least three has two distinct neighbours, both different from any given vertex.

theorem SimpleGraph.exists_adj_adj_ne_of_three_le_degree {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ↑(G.neighborSet v)] (hv : 3 ≤ G.degree v) (x : V) : ∃ (a : V) (b : V), G.Adj v a ∧ G.Adj v b ∧ a ≠ b ∧ a ≠ x ∧ b ≠ x

Two distinct neighbours of v other than a given vertex x, from a degree of at least three.