# Disjoint decomposition formalization

Lean formalization for `A Note on Disjoint Decompositions of [0,1) into Closed Sets`.

It is checked with Lean 4.30.0-rc2 and mathlib v4.30.0-rc2.

```powershell
lake exe cache get DisjointDecomposition.lean
lake build
```