Cuts of simple graphs

SimpleGraph.crossingFinset S is the set of edges of a finite simple graph with exactly one endpoint in S. An upstreaming candidate.

noncomputable def SimpleGraph.crossingFinset {W : Type u_1} (H : SimpleGraph W) [Fintype ↑H.edgeSet] (S : Finset W) : Finset (Sym2 W)

The edges of a simple graph with exactly one endpoint in S.

Equations

• H.crossingFinset S = {e ∈ H.edgeFinset | ∃ (a : W) (b : W), e = s(a, b) ∧ a ∈ S ∧ b ∉ S}

theorem SimpleGraph.mem_crossingFinset {W : Type u_1} {H : SimpleGraph W} [Fintype ↑H.edgeSet] {S : Finset W} {e : Sym2 W} : e ∈ H.crossingFinset S ↔ e ∈ H.edgeSet ∧ ∃ (a : W) (b : W), e = s(a, b) ∧ a ∈ S ∧ b ∉ S

theorem SimpleGraph.mem_crossingFinset_mk {W : Type u_1} {H : SimpleGraph W} [Fintype ↑H.edgeSet] {S : Finset W} {a b : W} : s(a, b) ∈ H.crossingFinset S ↔ H.Adj a b ∧ (a ∈ S ∧ b ∉ S ∨ b ∈ S ∧ a ∉ S)

An edge crosses S exactly when it is an edge with one endpoint on each side.

theorem SimpleGraph.crossingFinset_subset_edgeFinset {W : Type u_1} {H : SimpleGraph W} [Fintype ↑H.edgeSet] (S : Finset W) : H.crossingFinset S ⊆ H.edgeFinset

theorem SimpleGraph.crossingFinset_eq_empty_of_subsingleton {W : Type u_1} {H : SimpleGraph W} [Fintype ↑H.edgeSet] [Subsingleton W] (S : Finset W) : H.crossingFinset S = ∅

A graph with at most one vertex has no crossing edges.