From eb776c790e292077ca8920b3b70fcbc57a84a4ff Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 16:27:24 +0530 Subject: [PATCH] Fill that the Lebesgue boolean algebra is a sigma-algebra. Countable unions of Lebesgue measurable sets are Lebesgue measurable, which is the remaining axiom. --- Analysis/MeasureTheory/Section_1_4_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean index 51b417363..4629a0659 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