Proposition I.5.3 (可算性の特徴づけ)

• Proposition I.5.3 (可算性の特徴づけ) #Card
  • 可算であることの言い換え。

Back

$X$ が可算（$\mathbb{N}$ の像）$\iff$ 「有限かつ空でない」または $\operatorname{card} X = \aleph_0$。 証明 → 20_Literature/royal_road_to_topology/chapter1

Lean

Notes/ChapterI.lean : prop_I_5_3（(∃ f : ℕ → X, Surjective f) ↔ ((Finite X ∧ Nonempty X) ∨ Nonempty (X ≃ ℕ))）