countable_iff_nonempty_embedding — Mathlib

English

A type α is countable if and only if there exists a nonempty embedding α ↪ ℕ.

Русский

Тип α счётен тогда и только тогда, когда существует непустое вложение α ↪ ℕ.

LaTeX

$$$$ \operatorname{Countable}(\alpha) \iff \operatorname{Nonempty}(\alpha \hookrightarrow \mathbb{N}) $$$$

Lean4

theorem countable_iff_nonempty_embedding : Countable α ↔ Nonempty (α ↪ ℕ) :=
  ⟨fun ⟨⟨f, hf⟩⟩ => ⟨⟨f, hf⟩⟩, fun ⟨f⟩ => ⟨⟨f, f.2⟩⟩⟩

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