diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean index 51b41736..4629a065 100644 --- a/Analysis/MeasureTheory/Section_1_4_2.lean +++ b/Analysis/MeasureTheory/Section_1_4_2.lean @@ -30,7 +30,7 @@ def ConcreteBooleanAlgebra.isAtomic.isSigmaAlgebra {X: Type*} {B: ConcreteBoolea /-- Exercise 1.4.11 -/ theorem LebesgueMeasurable.boolean_algebra.isSigmaAlgebra (d:ℕ) : (LebesgueMeasurable.boolean_algebra d).isSigmaAlgebra := - by sorry + fun E hE => LebesgueMeasurable.countable_union hE def LebesgueMeasurable.sigmaAlgebra (d:ℕ) : ConcreteSigmaAlgebra (EuclideanSpace' d) := (LebesgueMeasurable.boolean_algebra.isSigmaAlgebra d).toSigmaAlgebra