mathlib3 documentation

measure_theory.decomposition.unsigned_hahn

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 #

Tags #

Hahn decomposition

Hahn decomposition theorem