Natural_Number_Functions_are_Uncountable

Proved

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

computabilityproofwikiuncountable-sets

The set of all natural number one-variable functions $\set {f: \N \to \N}$ is uncountably infinite.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Natural_Number_Functions_are_Uncountable : ¬Countable (ℕ → ℕ) := by sorry

Source