Theorem WithTop.eq_of_forall_le_coe_iff

Modification history

2025-10-28 13:23
Mathlib/Order/WithBot.lean
feat(ENNReal): equality from comparing with nnreals (#30721) …
Added WithTop.eq_of_forall_le_coe_iffView on Github →