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