This is an unofficial reimagining of the Archive of Formal Proofs
The Hahn and Jordan Decomposition Theoremsby Marie Cousin, Mnacho Echenim and Hervé Guiol