Theorem not_covBy

Modification history

2026-08-22 08:59

Mathlib/Order/Cover.lean

feat(Mathlib/Order/SuccPred/Limit): more `WithTop` lemmas about `IsMin`/`CovBy`/`IsSuccLimit` (#38841)

Modified not_covBy View on Github →

2024-01-09 09:25

Mathlib/Order/Cover.lean

chore(Covby): rename `Covby` to `CovBy` (#9578) …

Added not_covBy View on Github →