The vertex boundary of one side of a cut

The boundary consists of vertices on the given side that have a neighbor on the other side. Its cardinality is at most the number of crossing edges.

noncomputable def Algebraic.Cutwidth.cutBoundary {W : Type} (H : SimpleGraph W) (S : Finset W) : Finset W

Vertices of S incident to an edge crossing from S to its complement.

Equations

• Algebraic.Cutwidth.cutBoundary H S = {u ∈ S | ∃ v ∉ S, H.Adj u v}

theorem Algebraic.Cutwidth.mem_cutBoundary {W : Type} (H : SimpleGraph W) {S : Finset W} {u : W} : u ∈ cutBoundary H S ↔ u ∈ S ∧ ∃ v ∉ S, H.Adj u v

A boundary vertex is inside the side and has a neighbor outside.

theorem Algebraic.Cutwidth.cutBoundary_subset {W : Type} (H : SimpleGraph W) (S : Finset W) : cutBoundary H S ⊆ S

The boundary is contained in its side.