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
Instances For
    @[simp]
    theorem Sym2.sup_mk {α : Type u_1} [SemilatticeSup α] (a b : α) :
    s(a, b).sup = ab
    def Sym2.inf {α : Type u_1} [SemilatticeInf α] (x : Sym2 α) :
    α

    The infimum of the two elements.

    Equations
    Instances For
      @[simp]
      theorem Sym2.inf_mk {α : Type u_1} [SemilatticeInf α] (a b : α) :
      s(a, b).inf = ab
      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.

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