English
There is an isomorphism sumLexIicIoi between Iic x ⊕ Ioi x and α, obtained by combining a left-congruence on Iic x with the right component via RelIso sumLexComplRight.
Русский
Существует изоморфизм между Iic x ⊕ Ioi x и α, полученный сочетанием левой конгруэнции на Iic x с правой компонентой через RelIso sumLexComplRight.
LaTeX
$$$\\mathrm{sumLexIicIoi} : \\mathrm{Iic}\\, x \\oplus_\\mathrm{lex} \\mathrm{Ioi}\\, x \\cong_o \\alpha$$$
Lean4
/-- A linear order is isomorphic to the lexicographic sum of elements less or equal to `x` and
elements greater than `x`. -/
def sumLexIicIoi : Iic x ⊕ₗ Ioi x ≃o α :=
(sumLexCongr (setCongr (Iic x) {y | ¬x < y} (by ext; simp)) (refl _)).trans <|
ofRelIsoLT (RelIso.sumLexComplRight (· < ·) x)
