Treewidth, pathwidth, and treedepth of patterns
Lax461425.PatternWidths · concepts/Lax461425/PatternWidths.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The treewidth, pathwidth, and treedepth of a pattern are those of its underlying simple graph, so edge multiplicities play no role. A pattern has treewidth at most if it has a tree decomposition whose bags have at most vertices, and pathwidth at most if it has such a decomposition whose tree is a path. It has treedepth at most if it has an elimination forest in which every root-leaf path has at most vertices. The pattern without vertices has treewidth, pathwidth, and treedepth zero.
Concept map
Lean source view on GitHub
| 1 | import Lax228581.Treewidth |
| 2 | import Lax183560.TreeDepth |
| 3 | import Lax183560.Pathwidth |
| 4 | import Lax461425.HomomorphismPolynomials |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Treewidth, pathwidth, and treedepth of patterns |
| 9 | type: definition |
| 10 | --- |
| 11 | The treewidth, pathwidth, and treedepth of a pattern are those of its underlying simple graph, |
| 12 | so edge multiplicities play no role. A pattern has treewidth at most if it has a tree |
| 13 | decomposition whose bags have at most vertices, and pathwidth at most if it has |
| 14 | such a decomposition whose tree is a path. It has treedepth at most if it has an |
| 15 | elimination forest in which every root-leaf path has at most vertices. The pattern without |
| 16 | vertices has treewidth, pathwidth, and treedepth zero. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax461425.PatternWidths |
| 20 | |
| 21 | open HomomorphismPolynomials |
| 22 | |
| 23 | /-- The pattern has treewidth at most `k`: its underlying simple graph has a tree decomposition |
| 24 | with bags of size at most `k + 1`. -/ |
| 25 | def TreewidthLE (k : ℕ) (F : Pattern) : Prop := |
| 26 | Lax228581.Treewidth.HasTreewidthAtMost (underlying F) k |
| 27 | |
| 28 | /-- The pattern has pathwidth at most `k`: its underlying simple graph has a path |
| 29 | decomposition with bags of size at most `k + 1`. -/ |
| 30 | def PathwidthLE (k : ℕ) (F : Pattern) : Prop := |
| 31 | Lax183560.Pathwidth.HasPathwidthAtMost (underlying F) k |
| 32 | |
| 33 | /-- The pattern has treedepth at most `t`: its underlying simple graph lies in the closure of a |
| 34 | rooted forest in which every root-leaf path has at most `t` vertices. -/ |
| 35 | def TreedepthLE (t : ℕ) (F : Pattern) : Prop := |
| 36 | Lax183560.TreeDepth.HasTreedepthAtMost (underlying F) t |
| 37 | |
| 38 | end Lax461425.PatternWidths |
| 39 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments