Chord diagrams transport along monotone relabels

The label chord diagram of a relabeled system is the image of the original diagram under the order isomorphism, entrywise: the flags and the path matching are untouched, the labels shift through e, and e preserves the sorting.

theorem RS.relabel_boundaryLabel {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃o β) {W : Fragment α} (F : EdgeSubset W) {b : W.Flag} (hb : b ∈ (EdgeSubset.relabelUp e.toEquiv F).boundaryFlags) (hb' : b ∈ F.boundaryFlags) : (EdgeSubset.relabelUp e.toEquiv F).boundaryLabel hb = e (F.boundaryLabel hb')

The boundary label shifts through the relabel.