Commits on Aug 20, 2021

1. feat(data/finset,order/conditionally_complete_lattice): lemmas about … …

   …`min'/max'`
   
   * 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'`;
   * 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;
   * golf the proof of `filter.high_scores`.

   

   urkud committed Aug 20, 2021
   Configuration menu

   • View commit details
   • Copy full SHA for 8b0e59c
   • Browse repository at this point

   Copy the full SHA

   8b0e59c View commit details

   Browse the repository at this point in the history