refactor(measure_theory/decomposition): move decomposition into a f…

…older (#8374)

src/measure_theory/decomposition.lean → src/measure_theory/decomposition/unsigned_hahn.lean

@@ -2,13 +2,24 @@
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
+-/
+import measure_theory.measure_space
+
+/-!
+# Unsigned Hahn decomposition theorem
+
+This file proves the unsigned version of the Hahn decomposition theorem.
 
-Hahn decomposition theorem
+## Main statements
 
-TODO:
-* show general for signed measures (into ℝ)
+* `hahn_decomposition` : Given two finite measures `μ` and `ν`, there exists a measurable set `s`
+    such that any measurable set `t` included in `s` satisfies `ν t ≤ μ t`, and any
+    measurable set `u` included in the complement of `s` satisfies `μ u ≤ ν u`.
+
+## Tags
+
+Hahn decomposition
 -/
-import measure_theory.measure_space
 
 open set filter
 open_locale classical topological_space ennreal