Measurability of Set.encard and Set.ncard

In this file we prove that Set.encard and Set.ncard are measurable functions, provided that the ambient space is countable.

theorem measurable_encard {α : Type u_1} [Countable α] : Measurable Set.encard

theorem measurable_ncard {α : Type u_1} [Countable α] : Measurable Set.ncard