Bags meeting a connected vertex set

Lax263307.ConnectedBags · concepts/Lax263307/ConnectedBags.lean · lax-263307

proven

Loading review…

Natural Language Statement

Theorem

In a tree decomposition, the nodes whose bags meet a nonempty connected vertex set induce a connected subtree. The bag subtrees of adjacent vertices intersect in a bag covering their edge, so connected vertex sets give connected unions of bag subtrees.

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax263307.ConnectedBags

⊢Lax263307Proofs.ConnectedBags.meeting_connected

Lean source view on GitHub

Show types on hover

1	import Lax228581.Treewidth
2	import Mathlib.Data.Fintype.Fin
3
4	/-!
5	---
6	title: Bags meeting a connected vertex set
7	type: theorem
8	---
9	In a tree decomposition, the nodes whose bags meet a nonempty connected
10	vertex set induce a connected subtree. The bag subtrees of adjacent vertices
11	intersect in a bag covering their edge, so connected vertex sets give
12	connected unions of bag subtrees.
13
14	# Attribution
15
16	The connected-bag observation used in Bonnet–Chang, proof of Lemma 9.
17	-/
18
19	namespace Lax263307.ConnectedBags
20
21	open Lax228581.Treewidth
22
23	/-- The decomposition nodes whose bags meet `U`. -/
24	def meetingNodes {n : ℕ} {G : SimpleGraph (Fin n)}
25	(D : TreeDecomposition G) (U : Finset (Fin n)) : Set D.Node :=
26	{i \| ∃ v ∈ U, v ∈ D.bag i}
27
28	/-- Connected vertex sets meet a connected collection of decomposition bags. -/
29	axiom meeting_connected {n : ℕ} (G : SimpleGraph (Fin n))
30	(D : TreeDecomposition G) (U : Finset (Fin n))
31	(connected : (G.induce (↑U : Set (Fin n))).Connected) :
32	(D.tree.induce (meetingNodes D U)).Connected
33
34	end Lax263307.ConnectedBags
35