Measures of integer slabs

The measure of a null-measurable set is the sum of its measures in the integer slabs of a measurable real-valued function (TauCeti.measure_eq_tsum_inter_preimage_Ico).

theorem TauCeti.measure_eq_tsum_inter_preimage_Ico {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : Measurable f) {T : Set α} (hT : MeasureTheory.NullMeasurableSet T μ) : μ T = ∑' (m : ℤ), μ (T ∩ f ⁻¹' Set.Ico (↑m) (↑m + 1))

The measure of T is the sum of the measures of its slices m ≤ f x < m + 1, for m ∈ ℤ.