mathlib

40de4fcb - doc(order/bounds,order/conditionaly_complete_lattice): add some docs (#1686)

doc(order/bounds,order/conditionaly_complete_lattice): add some docs (#1686) * doc(order/bounds,order/conditionaly_complete_lattice): add some docs * Fixes by @jcommelin Co-Authored-By: Johan Commelin <johan@commelin.net> * Fix docs: `is_least` are not unique unless we have a partial order.