Commit 2021-09-18 10:03 0ee36a39
View on Github →feat(order/conditionally_complete_lattice): add lemmas (#9237)
- add lemmas about
conditionally_complete_linear_order_bot
; in this case we can drop somenonempty
assumptions; - add lemmas for the case of
[is_well_order α (<)]
; in this case infimum of a nonempty set is the least element of this set.