From 28bfc03c29a02f03acdd19e81afd676d9c40db9a Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:35:54 +0530 Subject: [PATCH] Fill countable additivity of restriction to a sub-sigma-algebra. --- Analysis/MeasureTheory/Section_1_4_3.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_3.lean b/Analysis/MeasureTheory/Section_1_4_3.lean index 60d13f856..cf7928cbd 100644 --- a/Analysis/MeasureTheory/Section_1_4_3.lean +++ b/Analysis/MeasureTheory/Section_1_4_3.lean @@ -175,7 +175,8 @@ theorem FinitelyAdditiveMeasure.isCountablyAdditive_restrict_alg {X:Type*} {B B' def CountablyAdditiveMeasure.restrict_alg {X:Type*} {B B': ConcreteSigmaAlgebra X} (μ: CountablyAdditiveMeasure B) (hBB' : B' ≤ B) : CountablyAdditiveMeasure B' := { toFinitelyAdditiveMeasure := μ.toFinitelyAdditiveMeasure.restrict_alg hBB', - measure_countable_additive := by sorry + measure_countable_additive := fun E hE hdisj => + μ.measure_countable_additive E (fun n => hBB' (E n) (hE n)) hdisj } /-- Example 1.4.29 (Dirac measure) -/