Theorem StrictMono.wellFoundedLT

Modification history

2024-11-04 23:57

Mathlib/Order/Monotone/Basic.lean

feat: generalize `Prod.wellFoundedLT/GT` to `Preorder`s (#17435) …

Modified StrictMono.wellFoundedLT View on Github →

2024-07-18 16:46

Mathlib/Order/WellFounded.lean

feat(Order/WellFounded): well-founded of strictly monotone (#14034) …

Added StrictMono.wellFoundedLT View on Github →