mathlib documentation

measure_theory.decomposition.unsigned_hahn

Unsigned Hahn decomposition theorem #

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

Main statements #

Tags #

Hahn decomposition

theorem measure_theory.hahn_decomposition {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure μ] [measure_theory.is_finite_measure ν] :
∃ (s : set α), measurable_set s (∀ (t : set α), measurable_set tt sν t μ t) ∀ (t : set α), measurable_set tt sμ t ν t

Hahn decomposition theorem