English
There is a RelIso between the Lex-ordered sum and the LT relation on the sum, given by toLex and its inverse toLex.
Русский
Существует отображение-релативно-изоморфизм между лексикографически упорядоченной суммой и отношением меньше на сумме, задаваемое toLex и его обратное.
LaTeX
$$$\text{toLexRelIsoLT} : Sum.Lex(\cdot<\cdot) (\cdot<\cdot) \simeq_r (\cdot<\cdot)$, с определениями toLex и ofLex.$$
Lean4
/-- `toLex` promoted to a `RelIso` between `<` relations. -/
def toLexRelIsoLT [LT α] [LT β] : Sum.Lex (· < · : α → α → Prop) (· < · : β → β → Prop) ≃r (· < · : α ⊕ₗ β → _ → _)
where
toFun := toLex
invFun := ofLex
map_rel_iff' := .rfl
