Isolated and universal creation steps for threshold graphs

The new vertex is the left Unit summand. Operations preserve the supplied partition; the elimination theorem supplies a reverse step in every nonempty finite threshold graph, without asserting a recognition algorithm.

def SimpleGraph.addIsolated {V : Type u_1} (G : SimpleGraph V) : SimpleGraph (Unit ⊕ V)

Add a single isolated vertex.

Equations

• G.addIsolated = ⊥ ⊕g G

def SimpleGraph.addUniversal {V : Type u_1} (G : SimpleGraph V) : SimpleGraph (Unit ⊕ V)

Add a single universal vertex, by complementing an isolated step.

Equations

• G.addUniversal = Gᶜ.addIsolatedᶜ

@[simp]

theorem SimpleGraph.addUniversal_adj_inr {V : Type u_1} {G : SimpleGraph V} (a b : V) : G.addUniversal.Adj (Sum.inr a) (Sum.inr b) ↔ G.Adj a b

The old vertices keep their adjacency in a universal step.

@[simp]

theorem SimpleGraph.addUniversal_adj_new {V : Type u_1} {G : SimpleGraph V} (a : V) : G.addUniversal.Adj (Sum.inl ()) (Sum.inr a)

The new universal vertex is adjacent to every old vertex.

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

Extend a split partition by putting the new isolated vertex in its independent part.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.ThresholdPartition.addIsolated {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) : G.addIsolated.ThresholdPartition

Add an isolated vertex to the supplied threshold partition.

Equations

• P.addIsolated = { toSplitPartition := P.addIsolated, nested := ⋯ }

def SimpleGraph.ThresholdPartition.addUniversal {V : Type u_1} {G : SimpleGraph V} (P : G.ThresholdPartition) : G.addUniversal.ThresholdPartition

Add a universal vertex using the complementary partition.

Equations

• P.addUniversal = P.compl.addIsolated.compl

theorem SimpleGraph.ThresholdPartition.exists_isolated_or_universal {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nonempty V] (P : G.ThresholdPartition) : ∃ (v : V), (∀ (u : V), ¬G.Adj v u) ∨ ∀ (u : V), u ≠ v → G.Adj v u

Every nonempty finite threshold partition has an isolated or universal vertex.