Theorem Order.IsSuccPrelimit.of_dense

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)

Modified Order.IsSuccPrelimit.of_dense View on Github →

2024-11-04 23:57

Mathlib/Order/SuccPred/Limit.lean

chore(SuccPred/Limit): rename 2 lemmas (#18462)

Added Order.IsSuccPrelimit.of_dense View on Github →