Skip to content

[Merged by Bors] - feat(Mathlib/Order/SuccPred/Limit): more WithTop lemmas about IsMin/CovBy/IsSuccLimit - #38841

Closed
SnirBroshi wants to merge 9 commits into
leanprover-community:masterfrom
SnirBroshi:feature/order/more-withtop-succ-limits
Closed

[Merged by Bors] - feat(Mathlib/Order/SuccPred/Limit): more WithTop lemmas about IsMin/CovBy/IsSuccLimit#38841
SnirBroshi wants to merge 9 commits into
leanprover-community:masterfrom
SnirBroshi:feature/order/more-withtop-succ-limits

add `not_covBy` and rename the existing one to `not_covBy_of_denselyO…

8a2749e
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Aug 21, 2026 in 1m 22s