Theorem Order.not_isPredLimit_iff_exists_covby

Modification history

2024-01-09 09:25
Mathlib/Order/SuccPred/Limit.lean
chore(Covby): rename `Covby` to `CovBy` (#9578) …
Deleted Order.not_isPredLimit_iff_exists_covbyView on Github →
2023-01-03 18:46
Mathlib/Order/SuccPred/Limit.lean
feat: port Order.SuccPred.Limit (#1300)
Added Order.not_isPredLimit_iff_exists_covbyView on Github →