English
If α is a preorder, α is unique, and β is equipped with a preorder/LE, then Lex(Prod α β) is order-isomorphic to β via the right projection, with inverse sending b to toLex (default, b).
Русский
Если α имеет предварительный порядок, элемент α уникален, и β имеет порядок, то Lex(Prod α β) изоморфно β по правой проекции, обратно — отображение b → toLex (default, b).
LaTeX
$$$\mathrm{uniqueProd}_{\alpha,\beta}: \mathrm{Lex}(\mathrm{Prod}\ \alpha\ \beta) \cong_o \beta$, с $\mathrm{toFun}(x)= (\mathrm{toLex}(x))_2$, $\mathrm{invFun}(b)= \mathrm{toLex}(\text{default}, b)$.$$
Lean4
/-- Lexicographic product type with `Unique` type on the left is `OrderIso` to the right. -/
def uniqueProd [Preorder α] [Unique α] [LE β] : α ×ₗ β ≃o β
where
toFun x := (ofLex x).2
invFun x := toLex (default, x)
left_inv x := x.rec fun (a, b) ↦ by simpa using Unique.default_eq a
right_inv x := by simp
map_rel_iff'
{a
b} :=
a.rec fun a ↦
b.rec fun b ↦ by
have heq : a.1 = b.1 := Subsingleton.allEq _ _
simp [Prod.Lex.toLex_le_toLex, heq]
