Documentation

Mathlib.Data.Sym.Sym2.Order

Sorting the elements of Sym2 #

This files 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.

Equations
  • x.sup = Sym2.lift fun (x1 x2 : α) => x1 x2, x
Instances For
    @[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.

    Equations
    • x.inf = Sym2.lift fun (x1 x2 : α) => x1 x2, x
    Instances For
      @[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
      @[simp]
      theorem Sym2.sortEquiv_apply_coe {α : Type u_1} [LinearOrder α] (s : Sym2 α) :
      (Sym2.sortEquiv s) = (s.inf, s.sup)
      @[simp]
      theorem Sym2.sortEquiv_symm_apply {α : Type u_1} [LinearOrder α] (p : { p : α × α // p.1 p.2 }) :
      Sym2.sortEquiv.symm p = Sym2.mk p
      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.

      Equations
      • Sym2.sortEquiv = { toFun := fun (s : Sym2 α) => (s.inf, s.sup), , invFun := fun (p : { p : α × α // p.1 p.2 }) => Sym2.mk p, left_inv := , right_inv := }
      Instances For