Lax18.FiniteGraphPartitions
Finite graph vertex partitions
concepts/Lax18/FiniteGraphPartitions.lean · lax-18
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A finite vertex partition is an indexed family of nonempty vertex sets which are pairwise disjoint and cover the whole vertex set. The indexing keeps the number of parts explicit, which is convenient for the regularity lemma.
An equitable partition is one in which any two parts have sizes differing by at most one. This is the clean textbook convention: there is no exceptional leftover class.
Lean source view on GitHub
| 1 | import Mathlib.Data.Finset.Basic |
| 2 | import Mathlib.Data.Finset.Card |
| 3 | import Mathlib.Data.Fintype.Basic |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Finite graph vertex partitions |
| 8 | type: definition |
| 9 | --- |
| 10 | A finite vertex partition is an indexed family of nonempty vertex sets which |
| 11 | are pairwise disjoint and cover the whole vertex set. The indexing keeps the |
| 12 | number of parts explicit, which is convenient for the regularity lemma. |
| 13 | |
| 14 | An equitable partition is one in which any two parts have sizes differing by |
| 15 | at most one. This is the clean textbook convention: there is no exceptional |
| 16 | leftover class. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax18.FiniteGraphPartitions |
| 20 | |
| 21 | universe u |
| 22 | |
| 23 | /-- An indexed partition of a finite vertex set. -/ |
| 24 | structure VertexPartition (V : Type u) [Fintype V] [DecidableEq V] where |
| 25 | /-- The number of parts. -/ |
| 26 | partCount : ℕ |
| 27 | /-- The part indexed by `i`. -/ |
| 28 | part : Fin partCount → Finset V |
| 29 | /-- Every part is nonempty. -/ |
| 30 | nonempty_part : ∀ i : Fin partCount, (part i).Nonempty |
| 31 | /-- Distinct parts are disjoint. -/ |
| 32 | pairwise_disjoint : |
| 33 | ∀ i j : Fin partCount, i ≠ j → Disjoint (part i) (part j) |
| 34 | /-- The parts cover all vertices. -/ |
| 35 | covers : ∀ v : V, ∃ i : Fin partCount, v ∈ part i |
| 36 | |
| 37 | namespace VertexPartition |
| 38 | |
| 39 | variable {V : Type u} [Fintype V] [DecidableEq V] |
| 40 | |
| 41 | /-- The size of a part of a vertex partition. -/ |
| 42 | def partSize (P : VertexPartition V) (i : Fin P.partCount) : ℕ := |
| 43 | (P.part i).card |
| 44 | |
| 45 | /-- A partition is equitable if any two part sizes differ by at most one. -/ |
| 46 | def Equitable (P : VertexPartition V) : Prop := |
| 47 | ∀ i j : Fin P.partCount, |
| 48 | P.partSize i ≤ P.partSize j + 1 ∧ |
| 49 | P.partSize j ≤ P.partSize i + 1 |
| 50 | |
| 51 | /-- A partition has exactly `k` parts. -/ |
| 52 | def HasPartCount (P : VertexPartition V) (k : ℕ) : Prop := |
| 53 | P.partCount = k |
| 54 | |
| 55 | end VertexPartition |
| 56 | |
| 57 | end Lax18.FiniteGraphPartitions |
| 58 |
Builds on
none
Used by
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments