Domain_of_Injection_to_Countable_Set_is_Countable
ProvedIf there is an injection from α to a countable set, then α is countable.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Domain_of_Injection_to_Countable_Set_is_Countable {α β : Type _} [Countable β] (f : α → β) (hf : Function.Injective f) : Countable α := by sorry