Commit 2022-06-27 21:32 cad1a6c6

feat(set_theory/cardinal/basic): lemmas about #(finset α) (#14850) This PR does the following:

• prove mk_finset_of_fintype : #(finset α) = 2 ^ℕ fintype.card α for fintype α
• rename mk_finset_eq_mk to mk_finset_of_infinite to match the former
• rename mk_finset to mk_coe_finset to avoid confusion with these two lemmas