Formalizing Structural Graph Theory in Lean 4

GraphClass. The source never defines “graph class” formally; it uses the phrase informally to mean a (possibly infinite) family of finite graphs. We encode this as a predicate polymorphic over the vertex type: ∀ {V : Type}, [DecidableEq V] → [Fintype V] → SimpleGraph V → Prop. The restriction to Type (universe 0) is intentional: all graphs in scope are finite, so universe polymorphism would add complexity with no benefit.

Scope. The source’s preliminaries also introduce distance-\(r\) independence and the vertex-deletion notation \(G - S\). In the catalog, those two notions are co-located with the definition that uses them and live in Definition UniformQuasiWideness.