Unordered pairs crossing a set

This file defines when an unordered pair has one endpoint in a set and the other endpoint outside the set. It also proves that one pair's weighted cut contribution is submodular, for use in pair and multigraph cut-capacity estimates.

Main definition

• Sym2.Crosses: an unordered pair crosses a set when its endpoints lie on opposite sides.

Main results

• Sym2.ite_crosses_union_add_ite_crosses_inter_le: one pair contributes a submodular cut weight.

def Sym2.Crosses {V : Type u_1} (p : Sym2 V) (S : Set V) : Prop

An unordered pair crosses S when its two endpoints lie on opposite sides of S.

@[simp]

theorem Sym2.crosses_mk_iff {V : Type u_1} {S : Set V} {x y : V} : s(x, y).Crosses S ↔ x ∈ S ∧ y ∉ S ∨ y ∈ S ∧ x ∉ S

A displayed unordered pair crosses a set exactly when its endpoints lie on opposite sides.

@[simp]

theorem Sym2.crosses_compl {V : Type u_1} (p : Sym2 V) (S : Set V) : p.Crosses Sᶜ ↔ p.Crosses S

Crossing a set is unchanged by exchanging the set with its complement.

theorem Sym2.not_crosses_diag {V : Type u_1} (x : V) (S : Set V) : ¬s(x, x).Crosses S

A diagonal unordered pair crosses no set.

theorem Sym2.Crosses.not_isDiag {V : Type u_1} {p : Sym2 V} {S : Set V} (h : p.Crosses S) : ¬p.IsDiag

A crossing unordered pair is not diagonal.

theorem Sym2.ite_crosses_union_add_ite_crosses_inter_le {V : Type u_1} {K : Type u_2} [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (p : Sym2 V) (a : K) (ha : ¬p.IsDiag → 0 ≤ a) (S T : Set V) [dU : Decidable (p.Crosses (S ∪ T))] [dI : Decidable (p.Crosses (S ∩ T))] [dS : Decidable (p.Crosses S)] [dT : Decidable (p.Crosses T)] : ((if p.Crosses (S ∪ T) then a else 0) + if p.Crosses (S ∩ T) then a else 0) ≤ (if p.Crosses S then a else 0) + if p.Crosses T then a else 0

The contribution of one unordered pair to a weighted cut is submodular when its weight is nonnegative off the diagonal. Diagonal weights are unrestricted.