English
There is a RelIso between the Lex-ordered sum Sum.Lex(≤) and the natural lexicographic order on the disjoint sum α ⊕β, whose forward map is the toLex construction and inverse is ofLex. This RelIso preserves the ≤ relations componentwise and translates between representations.
Русский
Существует взаимно однозначное отображение по порядкам между лексикографическим суммированием Sum.Lex(≤) и обычным лексикографическим порядком на сумме α ⊕β, где переход вперёд задаётся через toLex, а обратное — через ofLex; отображение сохраняет отношение порядка.
LaTeX
$$$toLexRelIsoLE : Sum.Lex(≤_α)(≤_β) \\to_r (≤_{α\\oplus_ℓ β})$ с forward = toLex и inv = ofLex, map_rel_iff' = rfl$$
Lean4
/-- `toLex` promoted to a `RelIso` between `≤` relations. -/
def toLexRelIsoLE [LE α] [LE β] : Sum.Lex (· ≤ · : α → α → Prop) (· ≤ · : β → β → Prop) ≃r (· ≤ · : α ⊕ₗ β → _ → _)
where
toFun := toLex
invFun := ofLex
map_rel_iff' := .rfl
