Lax17.Paths

Paths, linkages, and separators

concepts/Lax17/Paths.lean · lax-17

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A path is a simple finite walk with named endpoints. A vertex linkage is an indexed family of paths joining two terminal sets whose vertex sets are pairwise disjoint; an edge linkage asks instead that their edge sets be pairwise disjoint. Vertex and edge separators are finite sets meeting every path between the terminal sets.

All endpoint conventions are oriented. Reversing every path gives the corresponding unoriented formulation.

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Paths
2	import Mathlib.Combinatorics.SimpleGraph.Finite
3	import Mathlib.Data.Finset.Sym
4
5	/-!
6	---
7	title: Paths, linkages, and separators
8	type: definition
9	---
10	A path is a simple finite walk with named endpoints. A vertex linkage is an
11	indexed family of paths joining two terminal sets whose vertex sets are
12	pairwise disjoint; an edge linkage asks instead that their edge sets be
13	pairwise disjoint. Vertex and edge separators are finite sets meeting every
14	path between the terminal sets.
15
16	All endpoint conventions are oriented. Reversing every path gives the
17	corresponding unoriented formulation.
18	-/
19
20	namespace Lax17.Paths
21
22	universe u
23
24	/-- A simple finite path in `G`, with its orientation recorded. -/
25	structure Path {V : Type u} (G : SimpleGraph V) where
26	source : V
27	target : V
28	walk : G.Walk source target
29	simple : walk.IsPath
30
31	namespace Path
32
33	/-- The finite set of vertices used by a path. -/
34	noncomputable def vertices {V : Type u} [DecidableEq V] {G : SimpleGraph V}
35	(P : Path G) : Finset V :=
36	P.walk.support.toFinset
37
38	/-- The finite set of edges used by a path. -/
39	noncomputable def edges {V : Type u} [DecidableEq V] {G : SimpleGraph V}
40	(P : Path G) : Finset (Sym2 V) :=
41	P.walk.edges.toFinset
42
43	/-- `P` is oriented from `A` to `B`. -/
44	def Connects {V : Type u} [DecidableEq V] {G : SimpleGraph V}
45	(P : Path G) (A B : Finset V) : Prop :=
46	P.source ∈ A ∧ P.target ∈ B
47
48	/-- Every vertex of `P` lies in `C`. -/
49	def StaysIn {V : Type u} [DecidableEq V] {G : SimpleGraph V}
50	(P : Path G) (C : Finset V) : Prop :=
51	P.vertices ⊆ C
52
53	/-- The internal vertices of `P` avoid `X`. -/
54	def InternallyAvoids {V : Type u} [DecidableEq V] {G : SimpleGraph V}
55	(P : Path G) (X : Finset V) : Prop :=
56	∀ v ∈ P.vertices, v ∈ X → v = P.source ∨ v = P.target
57
58	end Path
59
60	/-- Exactly `k` pairwise vertex-disjoint paths oriented from `A` to `B`. -/
61	structure VertexLinkage {V : Type u} [DecidableEq V]
62	(G : SimpleGraph V) (A B : Finset V) (k : ℕ) where
63	path : Fin k → Path G
64	connects : ∀ i : Fin k, (path i).Connects A B
65	vertex_disjoint :
66	Pairwise fun i j => Disjoint (path i).vertices (path j).vertices
67
68	/-- Exactly `k` pairwise edge-disjoint paths oriented from `A` to `B`. -/
69	structure EdgeLinkage {V : Type u} [DecidableEq V]
70	(G : SimpleGraph V) (A B : Finset V) (k : ℕ) where
71	path : Fin k → Path G
72	connects : ∀ i : Fin k, (path i).Connects A B
73	edge_disjoint :
74	Pairwise fun i j => Disjoint (path i).edges (path j).edges
75
76	/-- A path joining two members of a linkage whose internal vertices avoid
77	every path of that linkage. -/
78	structure VertexLinkage.BridgeBetween
79	{V : Type u} [DecidableEq V]
80	{G : SimpleGraph V} {A B : Finset V} {k : ℕ}
81	(P : VertexLinkage G A B k) (i j : Fin k) where
82	path : Path G
83	source_on_first : path.source ∈ (P.path i).vertices
84	target_on_second : path.target ∈ (P.path j).vertices
85	internally_avoids_rows :
86	∀ r : Fin k, path.InternallyAvoids (P.path r).vertices
87
88	/-- Every two distinct paths of the linkage have a bridge contained in `C`. -/
89	def VertexLinkage.HasPairwiseBridgesIn
90	{V : Type u} [DecidableEq V]
91	{G : SimpleGraph V} {A B : Finset V} {k : ℕ}
92	(P : VertexLinkage G A B k) (C : Finset V) : Prop :=
93	∀ ⦃i j : Fin k⦄, i ≠ j →
94	∃ bridge : P.BridgeBetween i j, bridge.path.StaysIn C
95
96	/-- Edges of `G` with one endpoint in `X` and the other in `Y`. -/
97	noncomputable def edgeBoundary {V : Type u} [Fintype V] [DecidableEq V]
98	(G : SimpleGraph V) (X Y : Finset V) : Finset (Sym2 V) :=
99	@Finset.filter (Sym2 V)
100	(fun e => e ∈ G.edgeSet ∧ ∃ x ∈ X, ∃ y ∈ Y, e = s(x, y))
101	(Classical.decPred fun e =>
102	e ∈ G.edgeSet ∧ ∃ x ∈ X, ∃ y ∈ Y, e = s(x, y))
103	Finset.univ
104
105	/-- A partition of `C` separating `A` from `B` by fewer than `k` edges. -/
106	structure EdgeCutPartition {V : Type u} [Fintype V] [DecidableEq V]
107	(G : SimpleGraph V) (C A B : Finset V) (k : ℕ) where
108	left : Finset V
109	right : Finset V
110	cover : left ∪ right = C
111	disjoint : Disjoint left right
112	left_terminals : A ⊆ left
113	right_terminals : B ⊆ right
114	boundary_small : (edgeBoundary G left right).card < k
115
116	/-- A vertex set meeting every oriented `A`-to-`B` path. -/
117	def IsVertexSeparator {V : Type u} [DecidableEq V]
118	(G : SimpleGraph V) (A B X : Finset V) : Prop :=
119	∀ P : Path G, P.Connects A B →
120	∃ v ∈ P.vertices, v ∈ X
121
122	/-- An edge set meeting every oriented `A`-to-`B` path. -/
123	def IsEdgeSeparator {V : Type u} [DecidableEq V]
124	(G : SimpleGraph V) (A B : Finset V) (F : Finset (Sym2 V)) : Prop :=
125	∀ P : Path G, P.Connects A B →
126	∃ e ∈ P.edges, e ∈ F
127
128	end Lax17.Paths
129

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Paths, linkages, and separators

Flags

Flag this concept