mathlib
57e127a5 - refactor(order/complete_lattice): use `is_empty` (#8796)

Commit
4 years ago
refactor(order/complete_lattice): use `is_empty` (#8796) * change `set.univ_eq_empty_iff` to use `is_empty`; * rename `set.range_eq_empty` to `set.range_eq_empty_iff`; * add new `set.range_eq_empty`, it assumes `[is_empty α]`; * combine `supr_of_empty`, `supr_of_empty'`, and `supr_empty` into `supr_of_empty`, same for `infi`; * replace `csupr_neg` with `csupr_of_empty` and `csupr_false`; * adjust some proofs to use `casesI is_empty_of_nonempty α` instead of `by_cases h : nonempty α`.
Author
Parents
Loading