Commit 2020-02-25 14:16 450dcdf9
View on Github →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
andconditionally_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