Commit 2024-09-24 07:14 4d111f35

View on Github →

feat(Order/WellFounded): StrictMono.not_bddAbove_range (#16960) A strict monotonic function in an unbounded well-order has an unbounded range.

Estimated changes

Modified Mathlib/Order/SuccPred/Archimedean.lean

deleted theorem StrictAnti.not_bddAbove_range

deleted theorem StrictAnti.not_bddBelow_range

added theorem StrictAnti.not_bddBelow_range_of_isPredArchimedean

added theorem StrictAnti.not_bddBelow_range_of_isSuccArchimedean

deleted theorem StrictMono.not_bddAbove_range

added theorem StrictMono.not_bddAbove_range_of_isSuccArchimedean

deleted theorem StrictMono.not_bddBelow_range

added theorem StrictMono.not_bddBelow_range_of_isPredArchimedean

Modified Mathlib/Order/WellFounded.lean

added theorem StrictMono.not_bddAbove_range_of_wellFoundedLT

added theorem StrictMono.not_bddBelow_range_of_wellFoundedGT