Nested split partitions

Threshold membership is introduced using a split partition whose independent vertices have comparable neighborhoods. The equivalence with split membership and exclusion of induced P₄ is a theorem, not the definition.

def SimpleGraph.SplitPartition.HasNestedNeighborhoods {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) : Prop

The independent vertices have neighborhoods linearly ordered by inclusion.

Equations

• P.HasNestedNeighborhoods = ∀ u ∈ P.independent, ∀ v ∈ P.independent, G.neighborSet u ⊆ G.neighborSet v ∨ G.neighborSet v ⊆ G.neighborSet u

theorem SimpleGraph.SplitPartition.mem_clique_of_adj {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) {u v : V} (hu : u ∈ P.independent) (h : G.Adj u v) : v ∈ P.clique

Every neighbor of an independent vertex is in the clique part.

theorem SimpleGraph.SplitPartition.hasNestedNeighborhoods_of_isP4Free {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (h : G.IsP4Free) : P.HasNestedNeighborhoods

Excluding P₄ forces the independent neighborhoods to be comparable.

theorem SimpleGraph.SplitPartition.isP4Free_of_hasNestedNeighborhoods {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (hn : P.HasNestedNeighborhoods) : G.IsP4Free

In a split partition with nested neighborhoods, an induced P₄ is impossible.

theorem SimpleGraph.SplitPartition.hasNestedNeighborhoods_iff_isP4Free {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) : P.HasNestedNeighborhoods ↔ G.IsP4Free

The nested-neighborhood condition is precisely P₄ exclusion within split graphs.

def SimpleGraph.IsThreshold {V : Type u_1} (G : SimpleGraph V) : Prop

A threshold graph admits a split partition with nested independent neighborhoods.

Equations

• G.IsThreshold = ∃ (P : G.SplitPartition), P.HasNestedNeighborhoods

theorem SimpleGraph.isThreshold_iff_isSplit_and_isP4Free {V : Type u_1} {G : SimpleGraph V} : G.IsThreshold ↔ G.IsSplit ∧ G.IsP4Free

A structural characterization of threshold graphs within the split class.

theorem SimpleGraph.IsThreshold.compl {V : Type u_1} {G : SimpleGraph V} (h : G.IsThreshold) : Gᶜ.IsThreshold

Threshold membership is closed under complementation.

theorem SimpleGraph.IsThreshold.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsThreshold) (s : Set V) : (SimpleGraph.induce s G).IsThreshold

Every induced subgraph of a threshold graph is threshold.

theorem SimpleGraph.Iso.isThreshold_iff {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {H : SimpleGraph W} (f : G ≃g H) : G.IsThreshold ↔ H.IsThreshold

Graph isomorphisms preserve threshold membership.