The Földes–Hammer characterization of finite split graphs

Excluding induced 2K₂, C₄ and C₅ makes every cycle of length at least four have a chord. For finite graphs, the established simplicial reconstruction then gives a split partition. Both directions use native induced containment.

theorem SimpleGraph.isChordal_of_forbidden_induced_subgraphs {V : Type u_1} {G : SimpleGraph V} (hpair : ¬(⊤ ⊕g ⊤).IsIndContained G) (hfour : ¬(cycleGraph 4).IsIndContained G) (hfive : ¬(cycleGraph 5).IsIndContained G) : G.IsChordal

Excluding the three split obstructions implies chordality, without finiteness.

theorem SimpleGraph.isSplit_iff_forbidden_induced_subgraphs {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsSplit ↔ ¬(⊤ ⊕g ⊤).IsIndContained G ∧ ¬(cycleGraph 4).IsIndContained G ∧ ¬(cycleGraph 5).IsIndContained G

Földes–Hammer: a finite graph is split iff it excludes induced 2K₂, C₄ and C₅.

theorem SimpleGraph.pathGraph_four_isIndContained_cycleGraph_five : (pathGraph 4).IsIndContained (cycleGraph 5)

Four consecutive vertices in the five-cycle form an induced four-vertex path.

theorem SimpleGraph.isThreshold_iff_forbidden_induced_subgraphs {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsThreshold ↔ ¬(⊤ ⊕g ⊤).IsIndContained G ∧ ¬(cycleGraph 4).IsIndContained G ∧ ¬(pathGraph 4).IsIndContained G

A finite graph is threshold iff it excludes induced 2K₂, C₄ and P₄.