Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-28 16:13 4487e739

View on Github →

feat(order/bounded_lattice): is_total, coe_sup and unique_maximal lemmas (#6922) A few little additions for with_top and with_bot.

Estimated changes

added theorem eq_bot_of_minimal
added theorem eq_top_of_maximal
added theorem with_bot.coe_inf
added theorem with_bot.coe_sup