Theorem WithBot.isMax_coe_iff

Modification history

2026-08-22 08:59

Mathlib/Order/WithBot.lean

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

Added WithBot.isMax_coe_iff View on Github →