countable_iff_exists_surjective — Mathlib

English

Let s be a nonempty subset of α. Then s is countable iff there exists a surjection f: ℕ → s.

Русский

Пусть s — непустое подмножество α. Тогда s счетно тогда и только тогда, когда существует сюръекция f: ℕ → s.

LaTeX

$$$\\operatorname{Nonempty}(s) \\Rightarrow \\operatorname{Countable}(s) \\iff \\exists f:\\\\mathbb{N} \\to s,\\ \\operatorname{Surjective}(f)$$$

Lean4

/-- A non-empty set is countable iff there exists a surjection from the
natural numbers onto the subtype induced by the set.
-/
protected theorem countable_iff_exists_surjective {s : Set α} (hs : s.Nonempty) :
    s.Countable ↔ ∃ f : ℕ → s, Surjective f :=
  @countable_iff_exists_surjective s hs.to_subtype

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