Commit 2021-11-02 10:26 80dc445d

View on Github →

refactor(order/bounded_lattice): generalize le on with_{top,bot} (#10085) Before, some lemmas assumed preorder even when they were true for just the underlying le. In the case of with_bot, the missing underlying has_le instance is defined. For both with_{top,bot}, a few lemmas are generalized accordingly.

Estimated changes

Modified src/data/nat/cast.lean

Modified src/order/bounded_lattice.lean

modified theorem with_bot.coe_le

modified theorem with_bot.coe_le_coe

modified theorem with_bot.coe_lt_coe

modified theorem with_bot.some_le_some

modified theorem with_top.coe_le_coe

modified theorem with_top.coe_lt_coe

modified theorem with_top.coe_lt_top

modified theorem with_top.le_coe