mathlib documentation

measure_theory.decomposition

source
theorem measure_theory.hahn_decomposition {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} (hμ : ⇑μ set.univ < ⊤) (hν : ⇑ν set.univ < ⊤) :
∃ (s : set α), is_measurable s ∧ (∀ (t : set α), is_measurable t → t ⊆ s → ⇑ν t ≤ ⇑μ t) ∧ ∀ (t : set α), is_measurable t → t ⊆ sᶜ → ⇑μ t ≤ ⇑ν t