The Hahn and Jordan Decomposition Theorems

In this work we formalize the Hahn decomposition theorem for signed measures, namely that any measure space for a signed measure can be decomposed into a positive and a negative set, where every measurable subset of the positive one has a positive measure, and every measurable subset of the negative one has a negative measure. We also formalize the Jordan decomposition theorem as a corollary, which states that the signed measure under consideration admits a unique decomposition into a difference of two positive measures, at least one of which is finite.