Commit 2021-08-22 16:54 db9d4a3a

feat(data/finset,order/conditionally_complete_lattice): lemmas about min'/max' (#8782)

data/finset/*

• add finset.nonempty.to_set;
• add lemmas finset.max'_lt_iff, finset.lt_min'_iff, finset.max'_eq_sup', finset.min'_eq_inf';
• rewrite finset.induction_on_max without using finset.card, move one step to finset.lt_max'_of_mem_erase_max';

order/conditionally_complete_lattice

• add lemmas relating Sup/Inf of a nonempty finite set in a conditionally complete lattice to finset.sup'/finset.inf'/finset.max'/finset.min';
• a few more lemmas about Sup/Inf of a nonempty finite set in a conditionally complete lattice / linear order;

order/filter/at_top_bot

• golf the proof of filter.high_scores.