exists_surjective_nat — Mathlib

English

Let α be a nonempty countable type. Then there exists a surjective function f: ℕ → α.

Русский

Пусть α — непустой счётный множества; существует сюръекция f: ℕ → α.

LaTeX

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

Lean4

theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] : ∃ f : ℕ → α, Surjective f :=
  let ⟨f, hf⟩ := exists_injective_nat α
  ⟨invFun f, invFun_surjective hf⟩

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