Split partitions and chordal interfaces

Independent vertices are simplicial in a split graph. Every induced subgraph either contains such a vertex or is a clique. The existing elimination-order constructor therefore produces a perfect elimination order without a new graph representation or a duplicate proof of the chordal characterization.

theorem SimpleGraph.SplitPartition.exists_simplicial_in_finset {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (S : Finset V) (hS : S.Nonempty) : ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b

A split partition supplies a simplicial vertex in every nonempty finite set.

theorem SimpleGraph.IsSplit.exists_isPEO {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsSplit) : ∃ (ord : V → ℕ), G.IsPEO ord

A finite split graph has a perfect elimination order.

theorem SimpleGraph.IsSplit.isChordal {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsSplit) : G.IsChordal

Every finite split graph is chordal.

theorem SimpleGraph.IsSplit.isChordal_and_compl {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsSplit) : G.IsChordal ∧ Gᶜ.IsChordal

A finite split graph and its complement are both chordal.