uncountable_iff_forall_not_surjective

English

For a nonempty α, Uncountable α is equivalent to the statement that there is no surjection f: ℕ → α.

Русский

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

LaTeX

$$$\forall {\alpha}\,[\operatorname{Nonempty}(\alpha)]\ (\operatorname{Uncountable}(\alpha) \iff \forall f:\\mathbb{N} \to \alpha, \neg \operatorname{Surjective}(f))$$$

Lean4

theorem uncountable_iff_forall_not_surjective [Nonempty α] : Uncountable α ↔ ∀ f : ℕ → α, ¬Surjective f := by
  rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]

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