Commit 2019-11-17 17:46 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
Use ∈ *_bounds in the definition of conditionally_complete_lattice.

modified def lower_bounds

modified def upper_bounds

modified theorem bdd_above.mk

modified def bdd_above

modified theorem bdd_below.mk

modified def bdd_below