Label pairs sharing no label

One condition recurs wherever pairs of labels are handled: two pairs have all four of their labels distinct across the pair. It is what makes a chord diagram well formed, what lets a fold over a list of pairs be reordered, and what makes the symmetric-difference fold of a pair list its plain union. It is stated once here, with named fields, so that the four inequalities are never read off a nested conjunction by position.

structure RS.PairDisjoint {α : Type u_1} (p q : α × α) : Prop

Two label pairs sharing no label.

• fst_ne_fst : p.1 ≠ q.1

  The first labels differ.

• fst_ne_snd : p.1 ≠ q.2

  The first label of p is not the second of q.

• snd_ne_fst : p.2 ≠ q.1

  The second label of p is not the first of q.

• snd_ne_snd : p.2 ≠ q.2

  The second labels differ.

theorem RS.PairDisjoint.swap_left {α : Type u_1} {p q : α × α} (h : PairDisjoint p q) : PairDisjoint p.swap q

Sharing no label survives swapping the ends of the first pair.

theorem RS.PairDisjoint.swap_right {α : Type u_1} {p q : α × α} (h : PairDisjoint p q) : PairDisjoint p q.swap

Sharing no label survives swapping the ends of the second pair.