Commit 2022-07-08 02:55 6eeb941c

refactor(set_theory/cardinal/basic): migrate from fintype to finite (#15175)

• add finite_iff_exists_equiv_fin;
• add cardinal.mk_eq_nat_iff and cardinal.lt_aleph_0_iff_finite;
• rename the old cardinal.lt_aleph_0_iff_finite to cardinal.lt_aleph_0_iff_finite_set;
• rename cardinal.lt_aleph_0_of_fintype to cardinal.lt_aleph_0_of_finite, assume [finite] instead of [fintype];
• add an alias set.finite.lt_aleph_0;
• rename W_type.cardinal_mk_le_max_aleph_0_of_fintype to W_type.cardinal_mk_le_max_aleph_0_of_finite, fix assumption.