Commit 2020-07-24 09:01 6fe81bd5

chore(*): remove plift from some lemmas about infi/supr (#3503) Now supr_eq_supr_finset etc assume ι is a Type* and don't use plift. If you want to apply it to a Sort*, rewrite on equiv.plift.surjective.supr_comp first.

Full list of API changes:

data/equiv/basic

• equiv.ulift: change the order of universe arguments to match ulift;
• add coe_ulift, coe_plift, coe_ulift_symm, coe_plift_symm;

data/finset/lattice

• supr_eq_supr_finset, infi_eq_infi_finset: assume ι is a Type*, avoid plift;
• Union_eq_Union_finset, Inter_eq_Inter_finset: same as above;

data/set/basic

• function.surjective.range_comp: generalize to Sort* for 2 of 3 arguments;

order/complete_lattice

• remove supr_congr and infi_congr;
• add function.surjective.supr_comp and function.surjective.infi_comp.