nothing to prove
Definition
A graph class is a set of finite simple graphs. A class contains, for each number of vertices n, some of the simple graphs on the canonical n-element vertex type.
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Graph classes |
| 6 | type: definition |
| 7 | --- |
| 8 | A graph class is a set of finite simple graphs. A class contains, for |
| 9 | each number of vertices *n*, some of the simple graphs on the canonical |
| 10 | *n*-element vertex type. |
| 11 | |
| 12 | # Formalization notes |
| 13 | |
| 14 | Every finite simple graph is isomorphic to a graph on some `Fin n`, so |
| 15 | ranging over the canonical carriers loses no generality. Closure under |
| 16 | isomorphism is deliberately not required: no statement of this |
| 17 | submission needs it, and all hypotheses range over concrete members. |
| 18 | `GraphClass` is an abbreviation, so class membership is plain |
| 19 | application `C n G` throughout the submission. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax5.GraphClasses |
| 23 | |
| 24 | /-- A class of finite simple graphs: for each number of vertices `n`, a |
| 25 | predicate on the simple graphs over the canonical `n`-element type. -/ |
| 26 | abbrev GraphClass : Type := ∀ n : ℕ, SimpleGraph (Fin n) → Prop |
| 27 | |
| 28 | /-- The class of all finite simple graphs. -/ |
| 29 | def allGraphs : GraphClass := fun _ _ => True |
| 30 | |
| 31 | end Lax5.GraphClasses |
| 32 |
Formalization notes
Every finite simple graph is isomorphic to a graph on some Fin n, so
ranging over the canonical carriers loses no generality. Closure under
isomorphism is deliberately not required: no statement of this
submission needs it, and all hypotheses range over concrete members.
GraphClass is an abbreviation, so class membership is plain
application C n G throughout the submission.
Imported
none