English
A linear order is isomorphic to the lexicographic sum of elements less than x and elements greater or equal to x.
Русский
Линейный порядок изоморфен лексикографической сумме элементов меньше x и элементов, больших или равных x.
LaTeX
$$$\\mathrm{sumLexIioIci} : \\; \\mathrm{Iio}\\, x \\oplus_\\mathrm{lex} \\mathrm{Ici}\\, x \\simeq_o \\alpha$$$
Lean4
/-- A linear order is isomorphic to the lexicographic sum of elements less than `x` and elements
greater or equal to `x`. -/
def sumLexIioIci : Iio x ⊕ₗ Ici x ≃o α :=
(sumLexCongr (refl _) (setCongr (Ici x) {y | ¬y < x} (by ext; simp))).trans <|
ofRelIsoLT (RelIso.sumLexComplLeft (· < ·) x)
