countable_iff_exists_surjective — Mathlib

English

For every nonempty α, α is countable if and only if there exists a surjective function f: ℕ → α.

Русский

Для любого непустого α справедливо: α счётно тогда и только тогда, когда существует сюръекция f: ℕ → α.

LaTeX

$$$\forall \alpha\,(\operatorname{Nonempty}(\alpha) \rightarrow (\operatorname{Countable}(\alpha) \iff \exists f:\\mathbb{N} \to \alpha, \operatorname{Surjective}(f))))$$$

Lean4

theorem countable_iff_exists_surjective [Nonempty α] : Countable α ↔ ∃ f : ℕ → α, Surjective f :=
  ⟨@exists_surjective_nat _ _, fun ⟨_, hf⟩ ↦ hf.countable⟩

Похожие утверждения