mathlib documentation

measure_theory.decomposition

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