Commit 2026-08-22 08:59 169f50d4

View on Github →

feat(Mathlib/Order/SuccPred/Limit): more WithTop lemmas about IsMin/CovBy/IsSuccLimit (#38841)

Estimated changes

modified theorem WithTop.coe_covBy_coe
modified theorem WithTop.coe_wcovBy_coe
modified theorem WithTop.covBy_top_iff
added theorem WithTop.not_top_covBy
added theorem WithTop.wcovBy_top_iff
modified theorem not_covBy
added theorem top_wcovBy_iff
modified theorem WithTop.isSuccPrelimit_iff
modified theorem WithTop.isSuccPrelimit_top
added theorem WithBot.isMax_coe_iff
added theorem WithBot.isMax_iff
added theorem WithBot.not_isMax_top