Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 01:13 7ba9c3fe

View on Github →

feat(order/basic): More order instances for subtype (#13134) Add the has_le, has_lt, decidable_le, decidable_lt, bounded_order instances. Incorporating the decidable_le and decidable_lt instances into the linear_order one breaks some defeqs with ite/dite.

Estimated changes

modified theorem subtype.coe_le_coe
modified theorem subtype.coe_lt_coe
modified theorem subtype.mk_le_mk
modified theorem subtype.mk_lt_mk