Prove2Me

Infinite_Set_has_Countably_Infinite_Subset

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

countable-setsinfinite-set-has-countably-infinite-subsetinfinite-setsproofwikisubsets

Every infinite set has a countably infinite subset.

Preamble
import Mathlib.Data.Fintype.Card
Formal statement
theorem Infinite_Set_has_Countably_Infinite_Subset {S : Type _} [Infinite S] : ∃ f : ℕ → S, Function.Injective f := by sorry
Source
https://proofwiki.org/wiki/Infinite_Set_has_Countably_Infinite_Subset

View graph