Commit 2024-11-04 23:57 ba40da6e

View on Github →

feat: generalize Prod.wellFoundedLT/GT to Preorders (#17435) .. using a standard antisymmetrization trick. Also

Add lemmas wellFoundedLT/GT_antisymmetrization_iff.
Establish the OrderIso between the antisymmetrization of a product preorder and the product of antisymmetrizations.
Golf the original Prod.wellFoundedLT and rename it to Prod.wellFoundedLT'.
Golf StrictMono.wellFoundedLT etc. and move to where StrictMono is defined.

Estimated changes

Modified Mathlib/Order/Antisymmetrization.lean

added def Antisymmetrization.prodEquiv

added theorem Antisymmetrization.prodEquiv_apply_mk

added theorem Antisymmetrization.prodEquiv_symm_apply_mk

added theorem wellFoundedGT_antisymmetrization_iff

added theorem wellFoundedLT_antisymmetrization_iff

Modified Mathlib/Order/Monotone/Basic.lean

added theorem StrictAnti.wellFoundedGT

added theorem StrictAnti.wellFoundedLT

added theorem StrictMono.wellFoundedGT

added theorem StrictMono.wellFoundedLT

Modified Mathlib/Order/RelClasses.lean

added theorem Prod.wellFoundedGT'

added theorem Prod.wellFoundedLT'

Modified Mathlib/Order/WellFounded.lean

deleted theorem StrictAnti.wellFoundedGT

deleted theorem StrictAnti.wellFoundedLT

deleted theorem StrictMono.wellFoundedGT

deleted theorem StrictMono.wellFoundedLT