Prove2Me

Countable_Sets_Have_Measure_Zero

Proved

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

countable-setslebesgue-measuremeasure-theoryproofwiki

Every countable subset of the reals has Lebesgue measure zero.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

theorem Countable_Sets_Have_Measure_Zero (S : Set ℝ) (hS : S.Countable) : MeasureTheory.volume S = 0 := by sorry
Source
https://proofwiki.org/wiki/Countable_Sets_Have_Measure_Zero

View graph