Commit 2025-04-18 16:28 76a9f011

View on Github →

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

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.eq_of_forall_natCast_le_iff

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.eq_of_forall_le_coe_iff

added theorem WithBot.forall_le_coe_iff_le

added theorem WithTop.eq_of_forall_coe_le_iff

modified theorem WithTop.forall_coe_le_iff_le