Power_Set_of_Natural_Numbers_is_not_Countable

Proved

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

natural-numberspower-setproofwikiuncountable-sets

The power set $\powerset \N$ of the natural numbers $\N$ is not countable.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Power_Set_of_Natural_Numbers_is_not_Countable : ¬ Countable (Set ℕ) := by sorry

Source