Commit 2025-12-24 15:23 4d157708

View on Github →

chore(Order/WithBot): add to_dual attributes (part 3) (#32499) We dualize various instances on WithBot and WithTop. Most of these can unfortunately not (yet) be auto-generated, so we just mark them with to_dual existing.

Estimated changes

Modified Mathlib/Order/WithBot.lean

modified theorem WithBot.coe_inf

modified theorem WithBot.coe_max

modified theorem WithBot.coe_min

modified theorem WithBot.coe_sup

added theorem WithBot.lt_iff_exists_coe_btwn'

deleted theorem WithTop.coe_inf

deleted theorem WithTop.coe_max

deleted theorem WithTop.coe_min

deleted theorem WithTop.coe_sup

modified theorem WithTop.denselyOrdered_iff

deleted theorem WithTop.ge_of_forall_gt_iff_ge

deleted theorem WithTop.le_of_forall_lt_iff_le

deleted theorem WithTop.lt_iff_exists_coe_btwn