Commit 2026-03-12 18:27 b6176c7c

View on Github →

chore(Order/OrderDual): move material on OrderDual (#35150) This PR moves material about OrderDual from Mathlib.Order.Synonym to Mathlib.Order.OrderDual, so that these two files become independent. This way, Mathlib.Order.Synonym will not be on the long pole. Note: it seems that the file Mathlib.Order.Synonym used to define OrderDual. Maybe that file should now be renamed to Order.Lex?

Estimated changes

added theorem Colex.exists
added theorem Colex.forall
added def Colex
added theorem Lex.exists
added theorem Lex.forall
added def Lex
added def ofColex
added theorem ofColex_inj
added theorem ofColex_symm_eq
added theorem ofColex_toColex
added def ofLex
added theorem ofLex_inj
added theorem ofLex_symm_eq
added theorem ofLex_toLex
added def toColex
added theorem toColex_inj
added theorem toColex_ofColex
added theorem toColex_symm_eq
added def toLex
added theorem toLex_inj
added theorem toLex_ofLex
added theorem toLex_symm_eq
added theorem OrderDual.ext
added theorem OrderDual.le_toDual
added theorem OrderDual.lt_toDual
added def OrderDual.ofDual
added theorem OrderDual.ofDual_inj
added def OrderDual.toDual
added theorem OrderDual.toDual_inj
deleted theorem Colex.exists
deleted theorem Colex.forall
deleted def Colex
deleted theorem Lex.exists
deleted theorem Lex.forall
deleted def Lex
deleted theorem OrderDual.ext
deleted theorem OrderDual.le_toDual
deleted theorem OrderDual.lt_toDual
deleted def OrderDual.ofDual
deleted theorem OrderDual.ofDual_inj
deleted theorem OrderDual.ofDual_symm_eq
deleted theorem OrderDual.ofDual_toDual
deleted def OrderDual.toDual
deleted theorem OrderDual.toDual_inj
deleted theorem OrderDual.toDual_ofDual
deleted theorem OrderDual.toDual_symm_eq
deleted def ofColex
deleted theorem ofColex_inj
deleted theorem ofColex_symm_eq
deleted theorem ofColex_toColex
deleted def ofLex
deleted theorem ofLex_inj
deleted theorem ofLex_symm_eq
deleted theorem ofLex_toLex
deleted def toColex
deleted theorem toColex_inj
deleted theorem toColex_ofColex
deleted theorem toColex_symm_eq
deleted def toLex
deleted theorem toLex_inj
deleted theorem toLex_ofLex
deleted theorem toLex_symm_eq