Theorem WithTop.isSuccLimit_top

Modification history

2026-05-01 13:07
Mathlib/Order/SuccPred/Limit.lean
feat: interactions between `IsSuccLimit` and `WithTop` (#38244)
Added WithTop.isSuccLimit_topView on Github →