Catalog/Sparsity/StrongColoringBoundByAdm/Contract.lean
| 1 | import Catalog.Sparsity.ColoringNumbers.Contract |
| 2 | import Catalog.Sparsity.Admissibility.Contract |
| 3 | |
| 4 | namespace Catalog.Sparsity.StrongColoringBoundByAdm |
| 5 | |
| 6 | variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V] |
| 7 | |
| 8 | /-- Lemma 2.5: the strong r-coloring number is bounded by a power of the |
| 9 | r-admissibility. -/ |
| 10 | axiom scol_le_one_add_adm_sub_one_pow (G : SimpleGraph V) (r : ℕ) : |
| 11 | Catalog.Sparsity.ColoringNumbers.scol G r ≤ |
| 12 | 1 + (Catalog.Sparsity.Admissibility.adm G r - 1) ^ r |
| 13 | |
| 14 | end Catalog.Sparsity.StrongColoringBoundByAdm |
| 15 |