countable_iff_nonempty_embedding

theorem countable_iff_nonempty_embedding : ∀ {α : Sort u}, Countable α ↔ Nonempty (α ↪ ℕ)

This theorem states that, for any arbitrary type `α`, `α` is countable if and only if there exists a nonempty embedding from `α` to the natural numbers `ℕ`. In more detail, this means that there is a one-to-one function (the embedding) from `α` to `ℕ` that covers at least one element of `α` (i.e., the embedding is nonempty), and this is equivalent to the condition of `α` being countable.

More concisely: A type `α` is countable if and only if there exists a one-to-one function from `α` to the natural numbers `ℕ`.