Catalog/Sparsity/Preliminaries/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | namespace Catalog.Sparsity.Preliminaries |
| 4 | |
| 5 | /-- A graph class is a predicate on finite simple graphs, where the vertex type |
| 6 | may vary. -/ |
| 7 | abbrev GraphClass := |
| 8 | ∀ {V : Type}, [DecidableEq V] → [Fintype V] → SimpleGraph V → Prop |
| 9 | |
| 10 | end Catalog.Sparsity.Preliminaries |
| 11 |