Theorem WithTop.coe_covBy_coe

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 WithTop.coe_covBy_coe View on Github →

2026-04-21 17:27

Mathlib/Order/Cover.lean

chore(Order/Interval/Set/WithBotTop): use `to_dual` (#38240)

Modified WithTop.coe_covBy_coe View on Github →

2024-08-23 15:37

Mathlib/Order/Cover.lean

feat(Order/Cover): add lemmas about `WithTop`/`WithBot` (#15487)

Added WithTop.coe_covBy_coe View on Github →