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} [Finite 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

theorem SimpleGraph.disjoint_image_val_universalVerts {V : Type u_1} {G : SimpleGraph V} (s : Set ↑G.deleteUniversalVerts.verts) : Disjoint (Subtype.val '' s) G.universalVerts

theorem SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union {V : Type u_1} {G : SimpleGraph V} {t : Set V} {s : Set ↑G.deleteUniversalVerts.verts} (K : G.deleteUniversalVerts.coe.ConnectedComponent) (h : t ⊆ G.universalVerts) (hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents) : Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard

A component of the graph with universal vertices is even if we remove a set of representatives of odd components and a subset of universal vertices.

This is because the number of vertices in the even components is not affected, and from odd components exactly one vertex is removed.