Real_Numbers_are_Uncountable

Proved

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

proofwikireal-numbersreal-numbers-are-uncountableuncountable-sets

The set of real numbers $\R$ is uncountably infinite.

Preamble

import Mathlib.Topology.Order.Basic
import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Real_Numbers_are_Uncountable : ¬ Set.Countable (Set.univ : Set ℝ) := by sorry

Source