Theorem Order.IsSuccPrelimit.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.IsSuccPrelimit.withTopCoe View on Github →

2026-05-01 13:07

Mathlib/Order/SuccPred/Limit.lean

feat: interactions between `IsSuccLimit` and `WithTop` (#38244)

Added Order.IsSuccPrelimit.withTopCoe View on Github →