feat: remove sigma-finiteness assumption in layercake formula (#7454)

Currently, the layercake formula for the Lebesgue integral assumes sigma-finiteness of the measure, while the layercake formula for the Bochner integral (and integrable functions) doesn't. At the cost of a more complicated proof, we remove the sigma-finiteness also from the Lebesgue measure case.



Co-authored-by: Kalle <kalle.kytola@aalto.fi>

Mathlib/Data/Set/Intervals/Disjoint.lean

@@ -41,12 +41,12 @@ theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
 #align set.Iic_disjoint_Ioc Set.Iic_disjoint_Ioc
 
 @[simp]
-theorem Ioc_disjoint_Ioc_same {a b c : α} : Disjoint (Ioc a b) (Ioc b c) :=
+theorem Ioc_disjoint_Ioc_same : Disjoint (Ioc a b) (Ioc b c) :=
   (Iic_disjoint_Ioc (le_refl b)).mono (fun _ => And.right) le_rfl
 #align set.Ioc_disjoint_Ioc_same Set.Ioc_disjoint_Ioc_same
 
 @[simp]
-theorem Ico_disjoint_Ico_same {a b c : α} : Disjoint (Ico a b) (Ico b c) :=
+theorem Ico_disjoint_Ico_same : Disjoint (Ico a b) (Ico b c) :=
   disjoint_left.mpr fun _ hab hbc => hab.2.not_le hbc.1
 #align set.Ico_disjoint_Ico_same Set.Ico_disjoint_Ico_same
 
@@ -60,6 +60,13 @@ theorem Iic_disjoint_Ici : Disjoint (Iic a) (Ici b) ↔ ¬b ≤ a :=
   disjoint_comm.trans Ici_disjoint_Iic
 #align set.Iic_disjoint_Ici Set.Iic_disjoint_Ici
 
+@[simp]
+theorem Ioc_disjoint_Ioi (h : b ≤ c) : Disjoint (Ioc a b) (Ioi c) :=
+  disjoint_left.mpr (fun _ hx hy ↦ (hx.2.trans h).not_lt hy)
+
+theorem Ioc_disjoint_Ioi_same : Disjoint (Ioc a b) (Ioi b) :=
+  Ioc_disjoint_Ioi le_rfl
+
 @[simp]
 theorem iUnion_Iic : ⋃ a : α, Iic a = univ :=
   iUnion_eq_univ_iff.2 fun x => ⟨x, right_mem_Iic⟩