Theorem WithTop.isPredPrelimit_iff

Modification history

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