feat(set_theory/cardinal_ordinal): cardinal.mk_finset_eq_mk (#3578)

Author: TwoFX

src/data/finset/basic.lean

@@ -1186,6 +1186,14 @@ rfl
 @[simp] theorem to_finset_cons {a : α} {l : list α} : to_finset (a :: l) = insert a (to_finset l) :=
 finset.eq_of_veq $ by by_cases h : a ∈ l; simp [finset.insert_val', multiset.erase_dup_cons, h]
 
+theorem to_finset_surjective : function.surjective (to_finset : list α → finset α) :=
+begin
+  refine λ s, ⟨quotient.out' s.val, finset.ext $ λ x, _⟩,
+  obtain ⟨l, hl⟩ := quot.exists_rep s.val,
+  rw [list.mem_to_finset, finset.mem_def, ←hl],
+  exact list.perm.mem_iff (quotient.mk_out l)
+end
+
 end list
 
 namespace finset

src/set_theory/cardinal_ordinal.lean

@@ -460,6 +460,11 @@ calc  mk (list α)
 ... = max (omega) (mk α) : mul_eq_max (le_refl _) H1
 ... = mk α : max_eq_right H1
 
+theorem mk_finset_eq_mk {α : Type u} (h : omega ≤ mk α) : mk (finset α) = mk α :=
+eq.symm $ le_antisymm (mk_le_of_injective (λ x y, finset.singleton_inj.1)) $
+calc mk (finset α) ≤ mk (list α) : mk_le_of_surjective list.to_finset_surjective
+... = mk α : mk_list_eq_mk h
+
 lemma mk_bounded_set_le_of_omega_le (α : Type u) (c : cardinal) (hα : omega ≤ mk α) :
   mk {t : set α // mk t ≤ c} ≤ mk α ^ c :=
 begin