Chordality of a graph glued along a retained clique

Eliminate a simplicial vertex outside the shared clique in the left piece, unless the current vertex set lies entirely in the right piece. The no-cross condition ensures that left-exclusive vertices acquire no extra neighbours. The existing simplicial-elimination ranking then yields a PEO and chordality.

theorem SimpleGraph.IsChordal.induce_finset_subset {V : Type u_1} {G : SimpleGraph V} {A S : Finset V} (hA : (SimpleGraph.induce (↑A) G).IsChordal) (hSA : S ⊆ A) : (SimpleGraph.induce (↑S) G).IsChordal

Chordality of an induced piece passes to an induced subset of that piece.

theorem SimpleGraph.IsChordal.exists_relative_simplicial {V : Type u_1} {G : SimpleGraph V} {S : Finset V} (hS : (SimpleGraph.induce (↑S) G).IsChordal) (hSne : S.Nonempty) : ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b

A nonempty chordal induced vertex set contains a relative simplicial vertex.

theorem SimpleGraph.CliqueGluing.exists_relative_simplicial {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] {A B : Finset V} (h : G.CliqueGluing A B) (hA : (induce (↑A) G).IsChordal) (hB : (induce (↑B) G).IsChordal) (S : Finset V) (hSne : S.Nonempty) : ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b

Every remaining nonempty vertex set admits simplicial elimination when both induced pieces are chordal. The shared clique is retained until needed.

theorem SimpleGraph.CliqueGluing.isChordal {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] {A B : Finset V} (h : G.CliqueGluing A B) (hA : (induce (↑A) G).IsChordal) (hB : (induce (↑B) G).IsChordal) : G.IsChordal

Gluing chordal induced pieces along a retained clique preserves chordality.

theorem SimpleGraph.CliqueGluing.isChordal_iff {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] {A B : Finset V} (h : G.CliqueGluing A B) : G.IsChordal ↔ (induce (↑A) G).IsChordal ∧ (induce (↑B) G).IsChordal

A graph glued along a retained clique is chordal exactly when both pieces are.

theorem SimpleGraph.CliqueGluing.nonempty_cliqueTree {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] {A B : Finset V} (h : G.CliqueGluing A B) (hA : (induce (↑A) G).IsChordal) (hB : (induce (↑B) G).IsChordal) : Nonempty (G.CliqueTree V)

The glued graph admits a clique forest on its original vertex type. This constructs a fresh forest from an elimination order, not a graft of supplied trees.