fixes math-comp#1045

affeldt-aist · Oct 9, 2023 · 25006bf · 25006bf
1 parent 04dde36
commit 25006bf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -5548,7 +5548,7 @@ Qed.
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
 
-Section lebesgue_differentiation.
+Section lebesgue_differentiation_continuous.
 Context (rT : realType).
 Let mu := [the measure _ _ of @lebesgue_measure rT].
 Let R  := [the measurableType _ of measurableTypeR rT].
@@ -5631,4 +5631,4 @@ apply: le_trans.
 by rewrite ritv //= -EFinM lee_fin mulrC.
 Unshelve. all: by end_near. Qed.
 
-End lebesgue_differentiation.
+End lebesgue_differentiation_continuous.