Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 13:33 634dfc8a

View on Github →

feat(order/*): Missing order lifting instances (#12154) Add a few missing pullbacks of order instances.

Estimated changes

modified theorem binfi_sup_eq
modified theorem sup_binfi_eq
added def order_bot.lift
added def order_top.lift