Theorem OrderIso.sumLexIioIci_symm_apply_of_ge

Modification history

2025-07-04 21:33
Mathlib/Order/Hom/Lex.lean
feat: linear order is isomorphic to lexicographic sum of two intervals (#26613)
Added OrderIso.sumLexIioIci_symm_apply_of_geView on Github →