The decomposition step for cographs

Deleting a vertex from a connected P₄-free graph cannot leave several components unless that vertex is adjacent to every remaining vertex. This local statement will be used for the finite disconnection theorem.

theorem SimpleGraph.Preconnected.exists_neighbor_in_deleted_component {V : Type u_1} {G : SimpleGraph V} (hc : G.Preconnected) (v : V) (x : { u : V // u ≠ v }) : ∃ (y : { u : V // u ≠ v }), (induce {u : V | u ≠ v} G).Reachable x y ∧ G.Adj v ↑y

Every component after deletion meets the neighborhood of the deleted vertex.

theorem SimpleGraph.IsP4Free.adj_of_deleted_reachable {V : Type u_1} {G : SimpleGraph V} (hp : G.IsP4Free) (v : V) (x y z : { u : V // u ≠ v }) (hxy : (SimpleGraph.induce {u : V | u ≠ v} G).Reachable x y) (hxz : ¬(SimpleGraph.induce {u : V | u ≠ v} G).Reachable x z) (hvx : G.Adj v ↑x) (hvz : G.Adj v ↑z) : G.Adj v ↑y

An outside neighbor prevents a change of adjacency to the deleted vertex along a connected component: such a change would form an induced P₄.

theorem SimpleGraph.IsP4Free.adj_all_of_not_preconnected_delete {V : Type u_1} {G : SimpleGraph V} (hp : G.IsP4Free) (hc : G.Preconnected) (v : V) (hd : ¬(SimpleGraph.induce {u : V | u ≠ v} G).Preconnected) (x : V) : x ≠ v → G.Adj v x

A disconnected vertex deletion in a connected P₄-free graph makes the deleted vertex universal. No finiteness hypothesis is needed.

theorem SimpleGraph.not_preconnected_compl_of_universal {V : Type u_1} {G : SimpleGraph V} [Nontrivial V] (v : V) (hv : ∀ (x : V), x ≠ v → G.Adj v x) : ¬Gᶜ.Preconnected

A universal vertex is isolated in the complement, so that complement cannot be preconnected when there is another vertex.

theorem SimpleGraph.compl_induce_eq_induce_compl {V : Type u_1} {G : SimpleGraph V} (s : Set V) : (induce s G)ᶜ = induce s Gᶜ

Complementation commutes with induced restriction.

theorem SimpleGraph.IsP4Free.not_preconnected_or_compl {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (hp : G.IsP4Free) : ¬G.Preconnected ∨ ¬Gᶜ.Preconnected

Seinsche's decomposition theorem: a nontrivial finite P₄-free graph is disconnected or has disconnected complement.

theorem SimpleGraph.exists_separated_cut_of_not_preconnected {V : Type u_1} {G : SimpleGraph V} (hn : ¬G.Preconnected) : ∃ (s : Set V), s.Nonempty ∧ sᶜ.Nonempty ∧ ∀ u ∈ s, ∀ v ∉ s, ¬G.Adj u v

A disconnected graph has a nonempty proper vertex cut with no cross edges.