Lax9.BoundedMergeWidthLinearNeighborhoodComplexity
Linear Neighbourhood Complexity of Bounded Merge-Width Classes
concepts/Lax9/BoundedMergeWidthLinearNeighborhoodComplexity.lean · Lax9
Theorem
Every class of finite simple graphs with bounded merge-width has linear neighbourhood complexity.
Lean source view on GitHub
| 1 | import Lax9.MergeWidth |
| 2 | import Lax9.NeighborhoodComplexity |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Linear Neighbourhood Complexity of Bounded Merge-Width Classes |
| 7 | type: theorem |
| 8 | --- |
| 9 | Every class of finite simple graphs with bounded merge-width has linear |
| 10 | neighbourhood complexity. |
| 11 | -/ |
| 12 | |
| 13 | namespace Lax9.BoundedMergeWidthLinearNeighborhoodComplexity |
| 14 | |
| 15 | open Lax9.MergeWidth |
| 16 | open Lax9.NeighborhoodComplexity |
| 17 | |
| 18 | /-- Every graph class of bounded merge-width has linear neighbourhood |
| 19 | complexity. -/ |
| 20 | axiom bounded_mergeWidth_linearNeighborhoodComplexity |
| 21 | (C : GraphClass) (h : BoundedMergeWidth C) : LinearNeighborhoodComplexity C |
| 22 | |
| 23 | end Lax9.BoundedMergeWidthLinearNeighborhoodComplexity |
| 24 |
Imported by
none
Mathlib imports
none