Commit 2021-04-12 08:44 68e894dc

feat(finset/lattice): sup' is to sup as max' is to max (#7087) Introducing finset.sup', modelled on finset.max' but having no need for a linear_order. I wanted this for functions so also provide sup_apply and sup'_apply. By using cons instead of insert the axiom of choice is avoided throughout and I have replaced the proofs of three existing lemmas (sup_lt_iff, comp_sup_eq_sup_comp, sup_closed_of_sup_closed) that didn't need it. I have removed sup_subset entirely as it was surely introduced in ignorance of sup_mono.