English
Let α and β be types endowed with a strict total order. The canonical order isomorphism that interprets the lexicographic sum Sum.Lex with LT as the target relation has inverse given by the embedding of the left-right components, i.e. its inverse map coincides with the natural embedding of the left component (and similarly for the right component). In particular, the inverse correspondence is realized by the map ofLex.
Русский
Пусть α и β — множества с жёстким общим порядком. Каноническое отображение упорядочений между лексикографическим суммированием Sum.Lex и отношением LT имеет обратное отображение, заданное естественным вложением левой и правой частей; обратное отображение совпадает с отображением ofLex.
LaTeX
$$$toLexRelIsoLT^{-1} = ofLex$$$
Lean4
@[simp]
theorem toLexRelIsoLT_symm_coe [LT α] [LT β] : ⇑(toLexRelIsoLT (α := α) (β := β)).symm = ofLex :=
rfl
