Mathlib Changelog
v4
Changelog
About
Github
Theorem
StrictAnti.not_bddBelow_range_of_isPredArchimedean
Modification history
2026-02-22 13:15
Mathlib/Order/SuccPred/Archimedean.lean
chore(Order/SuccPred/Archimedean): use `to_dual` (#34882)
Deleted
StrictAnti.not_bddBelow_range_of_isPredArchimedean
View on Github →
2024-09-24 07:14
Mathlib/Order/SuccPred/Archimedean.lean
feat(Order/WellFounded): `StrictMono.not_bddAbove_range` (#16960) …
Added
StrictAnti.not_bddBelow_range_of_isPredArchimedean
View on Github →