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.

Equations

• x.sup = Sym2.lift ⟨fun (x1 x2 : α) => x1 ⊔ x2, ⋯⟩ x

@[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

@[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.

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 := ⋯ }

@[simp]

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

@[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.