Theorem WithTop.eq_of_forall_coe_le_iff

Modification history

2025-04-18 16:28

Mathlib/Order/WithBot.lean

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

Added WithTop.eq_of_forall_coe_le_iff View on Github →