Unsigned Hahn decomposition theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves the unsigned version of the Hahn decomposition theorem.
Main statements #
hahn_decomposition: Given two finite measuresμandν, there exists a measurable setssuch that any measurable settincluded inssatisfiesν t ≤ μ t, and any measurable setuincluded in the complement ofssatisfiesμ u ≤ ν u.
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 ν] :
Hahn decomposition theorem