Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-17 16:23 58f26a02

View on Github →

chore(order/bounded_lattice): trivial generalizations (#9246)

Estimated changes

modified theorem with_bot.coe_le
modified theorem with_bot.coe_lt_coe
modified theorem with_top.coe_le_coe
modified theorem with_top.coe_lt_coe
modified theorem with_top.coe_lt_iff
modified theorem with_top.coe_lt_top
modified theorem with_top.le_coe
modified theorem with_top.not_top_le_coe