Simplicial elimination outside a prescribed clique

In a finite chordal graph, a proper clique can be retained while some vertex outside it is eliminated. The proof works in the connected component of an outside vertex and uses the existing one- and two-vertex Dirac interfaces.

theorem SimpleGraph.ConnectedComponent.isSimplicial_coe {V : Type u_1} {G : SimpleGraph V} (c : G.ConnectedComponent) (x : ↥c) (hx : c.toSimpleGraph.IsSimplicial x) : G.IsSimplicial ↑x

Simpliciality inside a connected component is simpliciality in the whole graph.

theorem SimpleGraph.IsChordal.exists_isSimplicial_not_mem_clique {V : Type u_1} {G : SimpleGraph V} [Finite V] (hG : G.IsChordal) {S : Set V} (hS : G.IsClique S) (houtside : ∃ (u : V), u ∉ S) : ∃ z ∉ S, G.IsSimplicial z

A finite chordal graph has a simplicial vertex outside any proper clique.