Commit 2019-11-26 09:03 33df7e88
View on Github →feat(order/conditionally_complete_lattice): with_top (with_bot L) ins… (#1725)
- feat(order/conditionally_complete_lattice): with_top (with_bot L) instances
- dealing with most of Sebastien's comments
- initial defs. Now what happens?
- half way there
- compiles!
- tidy
- removing dead code
- docstring tinkering
- removing unused code
- is_lub_Sup' added
- refactor final proofs
- conforming to mathlib conventions
- def -> lemma