Verified Note

Disjoint Decompositions of [0,1)

A proof that the half-open interval cannot be written as a countable disjoint union of closed subsets of the real line.

Summary

Result and mechanism

The proof isolates a boundary obstruction after compactifying the half-open interval.

Main result

The set [0,1) is not a countable pairwise disjoint union of closed subsets of the real line.

Contribution type: Independent solution; Lean formalization
Contribution: Independent proof of the non-decomposition result via endpoint obstruction and Baire category, with the final statement formalized in Lean.
Mechanism: compactification, endpoint obstruction, Baire category
Lean theorem: no_pairwiseDisjoint_closed_iUnion_eq_Ico
Lean and mathlib: Lean 4.30.0-rc2, mathlib v4.30.0-rc2
Build command: lake build

PDF Lean source Lean check Verification index