Theorem StrictAnti.wellFoundedLT

Modification history

2024-11-04 23:57

Mathlib/Order/Monotone/Basic.lean

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

Modified StrictAnti.wellFoundedLT View on Github →

2024-07-18 16:46

Mathlib/Order/WellFounded.lean

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

Added StrictAnti.wellFoundedLT View on Github →