Commit 2025-07-04 21:33 0faf9c7e

View on Github →

feat: linear order is isomorphic to lexicographic sum of two intervals (#26613)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Hom/Lex.lean

added def OrderIso.sumLexIicIoi

added theorem OrderIso.sumLexIicIoi_apply_inl

added theorem OrderIso.sumLexIicIoi_apply_inr

added theorem OrderIso.sumLexIicIoi_symm_apply_Iic

added theorem OrderIso.sumLexIicIoi_symm_apply_Ioi

added theorem OrderIso.sumLexIicIoi_symm_apply_of_le

added theorem OrderIso.sumLexIicIoi_symm_apply_of_lt

added def OrderIso.sumLexIioIci

added theorem OrderIso.sumLexIioIci_apply_inl

added theorem OrderIso.sumLexIioIci_apply_inr

added theorem OrderIso.sumLexIioIci_symm_apply_Ici

added theorem OrderIso.sumLexIioIci_symm_apply_Iio

added theorem OrderIso.sumLexIioIci_symm_apply_of_ge

added theorem OrderIso.sumLexIioIci_symm_apply_of_lt

added def RelIso.sumLexComplLeft

added theorem RelIso.sumLexComplLeft_apply

added theorem RelIso.sumLexComplLeft_symm_apply

added def RelIso.sumLexComplRight

added theorem RelIso.sumLexComplRight_apply

added theorem RelIso.sumLexComplRight_symm_apply

Modified Mathlib/Order/Hom/Set.lean