Commit 2021-08-21 19:52 57e127a5

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 α.