Sorting the elements of Sym2

This file provides Sym2.sortEquiv, the forward direction of which is somewhat analogous to Multiset.sort.

def Sym2.sup {α : Type u_1} [SemilatticeSup α] (x : Sym2 α) : α

The supremum of the two elements.

@[simp]

theorem Sym2.sup_mk {α : Type u_1} [SemilatticeSup α] (a b : α) : s(a, b).sup = a ⊔ b

def Sym2.inf {α : Type u_1} [SemilatticeInf α] (x : Sym2 α) : α

The infimum of the two elements.

@[simp]

theorem Sym2.inf_mk {α : Type u_1} [SemilatticeInf α] (a b : α) : s(a, b).inf = a ⊓ b

theorem Sym2.inf_le_sup {α : Type u_1} [Lattice α] (s : Sym2 α) : s.inf ≤ s.sup

def Sym2.sortEquiv {α : Type u_1} [LinearOrder α] : Sym2 α ≃ { p : α × α // p.1 ≤ p.2 }

In a linear order, symmetric squares are canonically identified with ordered pairs.

@[simp]

theorem Sym2.sortEquiv_apply_coe {α : Type u_1} [LinearOrder α] (s : Sym2 α) : ↑(sortEquiv s) = (s.inf, s.sup)

@[simp]

theorem Sym2.sortEquiv_symm_apply {α : Type u_1} [LinearOrder α] (p : { p : α × α // p.1 ≤ p.2 }) : sortEquiv.symm p = s((↑p).1, (↑p).2)

theorem Sym2.inf_eq_inf_and_sup_eq_sup {α : Type u_1} [LinearOrder α] {s t : Sym2 α} : s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

In a linear order, two symmetric squares are equal if and only if they have the same infimum and supremum.