Theorem Order.IsPredLimit.withTopCoe

Modification history

2026-08-22 08:59
Mathlib/Order/SuccPred/Limit.lean
feat(Mathlib/Order/SuccPred/Limit): more `WithTop` lemmas about `IsMin`/`CovBy`/`IsSuccLimit` (#38841)
Deleted Order.IsPredLimit.withTopCoeView on Github →
2026-05-01 13:07
Mathlib/Order/SuccPred/Limit.lean
feat: interactions between `IsSuccLimit` and `WithTop` (#38244)
Added Order.IsPredLimit.withTopCoeView on Github →