Theorem WithBot.eq_of_forall_coe_le_iff

Modification history

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