Finite graph vertex partitions
Lax18.FiniteGraphPartitions · concepts/Lax18/FiniteGraphPartitions.lean · lax-18
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
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.
Concept map
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
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments