mathlib

1805f16a - refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit (#1691)

refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit (#1691) * refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit * Use `∈ *_bounds` in the definition of `conditionally_complete_lattice`.