# Unsigned Hahn decomposition theorem #

This file proves the unsigned version of the Hahn decomposition theorem.

## Main statements #

`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

theorem
MeasureTheory.hahn_decomposition
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:

∃ s,
MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ↑↑ν t ≤ ↑↑μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ↑↑μ t ≤ ↑↑ν t

**Hahn decomposition theorem**