Connectedness of a graph numbered so that neighbours descend

A graph on Fin n whose every vertex other than 0 has a neighbour with a smaller number is connected: a strong induction on the number of a vertex walks it down to 0. Numbering the vertices of a diagram this way is what makes connectedness of the Dynkin diagrams, finite and affine alike, a two-line check, and this file states the induction once for all of them.

Main results

• TauCeti.SimpleGraph.connected_fin_of_exists_adj_lt: a graph on Fin n in which every nonzero vertex has an adjacent vertex with a smaller number is connected.

theorem TauCeti.SimpleGraph.connected_fin_of_exists_adj_lt {n : ℕ} {G : SimpleGraph (Fin n)} (hn : 0 < n) (h : ∀ (i : Fin n), ↑i ≠ 0 → ∃ (j : Fin n), ↑j < ↑i ∧ G.Adj j i) : G.Connected

A graph on Fin n in which every vertex other than 0 has a neighbour with a smaller number is connected. Every vertex reaches 0 by descending along such neighbours.