Commit 2023-02-18 04:54 1912e881

View on Github →

feat: port Order.Extension.Well (#2333)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Extension/Well.lean

added theorem WellFounded.exists_well_order_ge

added def WellOrderExtension

added def toWellOrderExtension

added theorem toWellOrderExtension_strictMono

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/RelClasses.lean

added theorem WellFounded.prod_lex