mathlib

450dcdf9 - refactor(order/bounds): use dot notation, reorder, prove more properties (#2028)

refactor(order/bounds): use dot notation, reorder, prove more properties (#2028) * refactor(order/bounds): use dot notation, prove more properties Also make parts of `complete_lattice` and `conditionally_complete_lattice` use these lemmas. * Comments * Add a module docstring * Fixes from review, +4 lemmas about images * Fix a typo in the previous commit * Update src/order/bounds.lean * Update src/order/bounds.lean Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>