Documentation

Mathlib.Combinatorics.SimpleGraph.UniversalVerts

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 #

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

Equations
Instances For

    The subgraph of G with the universal vertices removed.

    Equations
    Instances For