# mathlibdocumentation

measure_theory.decomposition.unsigned_hahn

# 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 measure_theory.hahn_decomposition {α : Type u_1} {μ ν : measure_theory.measure α}  :
∃ (s : set α), (∀ (t : set α), t sν t μ t) ∀ (t : set α), t sμ t ν t

Hahn decomposition theorem