mathlib

3cc7a32b - feat(order/complete_lattice): add a constructor from `partial_order` and `Inf` (#2359)