Laminar families and crossing bipartitions of finite sets

Two finite sets are nested or disjoint if one contains the other or they do not meet. Two bipartitions cross if all four intersections of their sides are nonempty. Choosing the side avoiding a fixed root identifies pairwise non-crossing bipartitions with laminar families.

Main declarations

• Finset.NestedOrDisjoint: the relation defining laminar families.
• Finset.Crosses: crossing of the bipartitions determined by two finite sets.
• Finset.sideAvoiding: the side of a bipartition avoiding a chosen root.
• Finset.pairwise_nestedOrDisjoint_image_sideAvoiding: the root convention for a family.

References

• B. Korte and J. Vygen, Combinatorial Optimization: Theory and Algorithms, Section 8.6.
• D. Gusfield, Very Simple Methods for All Pairs Network Flow Analysis, SIAM J. Comput. 19 (1990), 143–155.

Laminar and crossing cuts

A family of sets is laminar when its members are pairwise nested or disjoint. Two cuts, viewed as bipartitions, cross when each side of one meets each side of the other. Choosing for every cut its side avoiding a fixed root vertex turns a pairwise non-crossing family of cuts into a laminar family. This lets uncrossing arguments for symmetric set functions work with laminar families.

def Finset.NestedOrDisjoint {V : Type u_1} (S T : Finset V) : Prop

Two sets are nested or disjoint when one contains the other or they do not meet. A family is laminar when its members are pairwise nested or disjoint.

theorem Finset.nestedOrDisjoint_def {V : Type u_1} {S T : Finset V} : S.NestedOrDisjoint T ↔ S ⊆ T ∨ T ⊆ S ∨ Disjoint S T

Two sets are nested or disjoint exactly when one contains the other or they do not meet.

theorem Finset.NestedOrDisjoint.of_subset {V : Type u_1} {S T : Finset V} (h : S ⊆ T) : S.NestedOrDisjoint T

A set is nested with every superset.

theorem Finset.NestedOrDisjoint.of_superset {V : Type u_1} {S T : Finset V} (h : T ⊆ S) : S.NestedOrDisjoint T

A set is nested with every subset.

theorem Finset.NestedOrDisjoint.of_disjoint {V : Type u_1} {S T : Finset V} (h : Disjoint S T) : S.NestedOrDisjoint T

Disjoint sets are nested or disjoint.

theorem Finset.nestedOrDisjoint_comm {V : Type u_1} {S T : Finset V} : S.NestedOrDisjoint T ↔ T.NestedOrDisjoint S

Being nested or disjoint is a symmetric relation.

theorem Finset.NestedOrDisjoint.symm {V : Type u_1} {S T : Finset V} (h : S.NestedOrDisjoint T) : T.NestedOrDisjoint S

Being nested or disjoint is a symmetric relation.

theorem Finset.NestedOrDisjoint.inter {V : Type u_1} [DecidableEq V] {S T U : Finset V} (hS : S.NestedOrDisjoint U) (hT : T.NestedOrDisjoint U) : (S ∩ T).NestedOrDisjoint U

Intersecting two sets preserves being nested with or disjoint from a third set.

theorem Finset.NestedOrDisjoint.union {V : Type u_1} [DecidableEq V] {S T U : Finset V} (hST : (S ∩ T).Nonempty) (hS : S.NestedOrDisjoint U) (hT : T.NestedOrDisjoint U) : (S ∪ T).NestedOrDisjoint U

The union of two meeting sets is nested with or disjoint from every set that is nested with or disjoint from both of them. Without a common element this fails: {1} and {2} are nested with or disjoint from {1, 3}, but {1, 2} is not.

def Finset.Crosses {V : Type u_1} (S T : Finset V) : Prop

Two cuts (S, Sᶜ) and (T, Tᶜ) cross when each side of one meets each side of the other.

theorem Finset.crosses_def {V : Type u_1} {S T : Finset V} : S.Crosses T ↔ (∃ v ∈ S, v ∈ T) ∧ (∃ v ∈ S, v ∉ T) ∧ (∃ v ∈ T, v ∉ S) ∧ ∃ v ∉ S, v ∉ T

Two cuts cross exactly when each side of one contains a vertex of each side of the other.

theorem Finset.crosses_iff {V : Type u_1} [Fintype V] [DecidableEq V] {S T : Finset V} : S.Crosses T ↔ (S ∩ T).Nonempty ∧ (S \ T).Nonempty ∧ (T \ S).Nonempty ∧ (Sᶜ ∩ Tᶜ).Nonempty

Two cuts cross exactly when the four intersections of their sides are nonempty.

theorem Finset.crosses_comm {V : Type u_1} {S T : Finset V} : S.Crosses T ↔ T.Crosses S

Crossing is a symmetric relation.

theorem Finset.Crosses.symm {V : Type u_1} {S T : Finset V} (h : S.Crosses T) : T.Crosses S

Crossing is a symmetric relation.

@[simp]

theorem Finset.crosses_compl_left {V : Type u_1} [Fintype V] [DecidableEq V] {S T : Finset V} : Sᶜ.Crosses T ↔ S.Crosses T

Crossing depends only on the bipartition, not on the side chosen for the first cut.

@[simp]

theorem Finset.crosses_compl_right {V : Type u_1} [Fintype V] [DecidableEq V] {S T : Finset V} : S.Crosses Tᶜ ↔ S.Crosses T

Crossing depends only on the bipartition, not on the side chosen for the second cut.

theorem Finset.NestedOrDisjoint.not_crosses {V : Type u_1} {S T : Finset V} (h : S.NestedOrDisjoint T) : ¬S.Crosses T

Nested or disjoint sets do not cross.

theorem Finset.not_crosses_iff_nestedOrDisjoint {V : Type u_1} {r : V} {S T : Finset V} (hS : r ∉ S) (hT : r ∉ T) : ¬S.Crosses T ↔ S.NestedOrDisjoint T

Root convention. Two sets avoiding a common vertex do not cross exactly when they are nested or disjoint: their union cannot cover all vertices.

theorem Finset.not_crosses_union {V : Type u_1} [DecidableEq V] {S T U : Finset V} (hST : (S ∩ T).Nonempty) (hSU : ¬S.Crosses U) (hTU : ¬T.Crosses U) : ¬(S ∪ T).Crosses U

Uncrossing preserves non-crossing. The union of two meeting sets crosses no cut that neither of them crosses.

def Finset.sideAvoiding {V : Type u_1} [Fintype V] [DecidableEq V] (r : V) (S : Finset V) : Finset V

The side of the cut (S, Sᶜ) not containing the root vertex r.

@[simp]

theorem Finset.notMem_sideAvoiding {V : Type u_1} [Fintype V] [DecidableEq V] (r : V) (S : Finset V) : r ∉ sideAvoiding r S

The side avoiding the root does not contain it.

@[simp]

theorem Finset.mem_sideAvoiding {V : Type u_1} [Fintype V] [DecidableEq V] {r v : V} {S : Finset V} : v ∈ sideAvoiding r S ↔ (v ∈ S ↔ r ∉ S)

A vertex lies in the side avoiding the root exactly when it lies on the opposite side of the cut from the root.

@[simp]

theorem Finset.sideAvoiding_of_notMem {V : Type u_1} [Fintype V] [DecidableEq V] {r : V} {S : Finset V} (h : r ∉ S) : sideAvoiding r S = S

A side not containing the root is its own side avoiding the root.

@[simp]

theorem Finset.sideAvoiding_of_mem {V : Type u_1} [Fintype V] [DecidableEq V] {r : V} {S : Finset V} (h : r ∈ S) : sideAvoiding r S = Sᶜ

The side avoiding the root of a side containing it is the complement.

@[simp]

theorem Finset.sideAvoiding_compl {V : Type u_1} [Fintype V] [DecidableEq V] (r : V) (S : Finset V) : sideAvoiding r Sᶜ = sideAvoiding r S

Both sides of a cut have the same side avoiding the root.

@[simp]

theorem Finset.crosses_sideAvoiding_left {V : Type u_1} [Fintype V] [DecidableEq V] {r : V} {S T : Finset V} : (sideAvoiding r S).Crosses T ↔ S.Crosses T

Replacing the first cut by its side avoiding the root does not affect crossing.

@[simp]

theorem Finset.crosses_sideAvoiding_right {V : Type u_1} [Fintype V] [DecidableEq V] {r : V} {S T : Finset V} : S.Crosses (sideAvoiding r T) ↔ S.Crosses T

Replacing the second cut by its side avoiding the root does not affect crossing.

theorem Finset.pairwise_nestedOrDisjoint_image_sideAvoiding {V : Type u_1} [Fintype V] [DecidableEq V] {𝒞 : Set (Finset V)} (h𝒞 : 𝒞.Pairwise fun (S T : Finset V) => ¬S.Crosses T) (r : V) : (sideAvoiding r '' 𝒞).Pairwise NestedOrDisjoint

Root convention. Representing each cut of a pairwise non-crossing family by its side avoiding a fixed root vertex gives a laminar family.