Theorem WithBot.eq_of_forall_le_coe_iff

Modification history

2025-04-18 16:28

Mathlib/Order/WithBot.lean

feat(Order/WithTop): criterion for equality in WithTop (#24165)

Added WithBot.eq_of_forall_le_coe_iff View on Github →