English
There is a canonical order-preserving bijection between Sym2 α and ordered pairs under a linear order: each Sym2 element corresponds to a pair (inf, sup) with inf ≤ sup.
Русский
Существуют каноническая биекция и упорядочение между Sym2 α и упорядоченными парами: каждый элемент Sym2 α соответствует паре (inf, sup) с inf ≤ sup.
LaTeX
$$$\mathrm{sortEquiv} : \mathrm{Sym}^2(\alpha) \simeq \{ p=(x,y) : \alpha\times\alpha \mid x \le y\}$$$
Lean4
/-- In a linear order, symmetric squares are canonically identified with ordered pairs. -/
@[simps!]
def sortEquiv [LinearOrder α] : Sym2 α ≃ { p : α × α // p.1 ≤ p.2 }
where
toFun s := ⟨(s.inf, s.sup), Sym2.inf_le_sup _⟩
invFun p := Sym2.mk p
left_inv :=
Sym2.ind fun a b =>
mk_eq_mk_iff.mpr <| by
cases le_total a b with
| inl h => simp [h]
| inr h => simp [h]
right_inv := Subtype.rec <| Prod.rec fun x y hxy => Subtype.ext <| Prod.ext (by simp [hxy]) (by simp [hxy])
