Universal Vertices

This file defines the set of universal vertices: those vertices that are connected to all others. In addition, it describes results when considering connected components of the graph where universal vertices are deleted. This particular graph plays a role in the proof of Tutte's Theorem.

Main definitions

• G.universalVerts is the set of vertices that are connected to all other vertices.
• G.deleteUniversalVerts is the subgraph of G with the universal vertices removed.

def SimpleGraph.universalVerts {V : Type u_1} (G : SimpleGraph V) : Set V

The set of vertices that are connected to all other vertices.

Equations

• G.universalVerts = {v : V | ∀ ⦃w : V⦄, v ≠ w → G.Adj w v}

theorem SimpleGraph.isClique_universalVerts {V : Type u_1} (G : SimpleGraph V) : G.IsClique G.universalVerts

def SimpleGraph.deleteUniversalVerts {V : Type u_1} (G : SimpleGraph V) : G.Subgraph

The subgraph of G with the universal vertices removed.

Equations

• G.deleteUniversalVerts = ⊤.deleteVerts G.universalVerts

@[simp]

theorem SimpleGraph.deleteUniversalVerts_adj {V : Type u_1} (G : SimpleGraph V) (u v : V) : G.deleteUniversalVerts.Adj u v = (u ∉ G.universalVerts ∧ v ∉ G.universalVerts ∧ G.Adj u v)

@[simp]

theorem SimpleGraph.deleteUniversalVerts_verts {V : Type u_1} (G : SimpleGraph V) : G.deleteUniversalVerts.verts = Set.univ \ G.universalVerts

theorem SimpleGraph.Subgraph.IsMatching.exists_of_universalVerts {V : Type u_1} {G : SimpleGraph V} [Fintype V] {s : Set V} (h : Disjoint G.universalVerts s) (hc : s.ncard ≤ G.universalVerts.ncard) : ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching