Infinite_if_Injection_from_Natural_Numbers

Proved

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

infinite-setsproofwikiset-theory

Let $S$ be a set. Let there exist an injection $\phi: \N \to S$ from the natural numbers to $S$ . Then $S$ is infinite.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Infinite_if_Injection_from_Natural_Numbers {S : Type _} (f : ℕ → S) (hf : Function.Injective f) : Infinite S := by sorry

Source