Commit 2025-10-01 13:25 52742777

View on Github →

feat: Colex type synonym (#29058) We create a new Colex type synonym for the colexicographic order on a type. We use this to re-define the colexicographic order on Finset, protecting and deprecating the existing Finset.Colex type synonym. A future PR will add instances for Pi types and Finsupp. See Zulip for some discussion on this.

Estimated changes

modified theorem Finset.Colex.le_def
modified theorem Finset.Colex.ofColex_bot
modified theorem Finset.Colex.ofColex_top
modified theorem Finset.Colex.toColex_mono
deleted structure Finset.Colex
deleted theorem Finset.ofColex_inj
modified theorem Finset.ofColex_injective
modified theorem Finset.ofColex_ne_ofColex
deleted theorem Finset.ofColex_toColex
modified def Finset.orderIsoColex
deleted theorem Finset.toColex_inj
modified theorem Finset.toColex_injective
modified theorem Finset.toColex_ne_toColex
deleted theorem Finset.toColex_ofColex
added theorem Colex.exists
added theorem Colex.forall
added def Colex
added def ofColex
added theorem ofColex_inj
added theorem ofColex_symm_eq
added theorem ofColex_toColex
added def toColex
added theorem toColex_inj
added theorem toColex_ofColex
added theorem toColex_symm_eq