From ce361ef1578f17a18b67a9980d5d47a558931fd6 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 12 Aug 2026 21:51:30 +0530 Subject: [PATCH] fix: the Jordan algebra is a sigma-algebra when d = 0 EuclideanSpace' 0 is a one-point space, so every subset of it (there are only two) is Jordan measurable and the Jordan algebra is all of the power set, which is trivially closed under countable unions. The negative statement therefore only holds in positive dimension. The neighbouring Exercise 1.4.5 statements in Section_1_4_1 and JordanMeasurable.not_borel below already carry the same d >= 1 hypothesis. Signed-off-by: Taksh --- Analysis/MeasureTheory/Section_1_4_2.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean index e154b7e01..51b417363 100644 --- a/Analysis/MeasureTheory/Section_1_4_2.lean +++ b/Analysis/MeasureTheory/Section_1_4_2.lean @@ -41,7 +41,8 @@ theorem IsNull.boolean_algebra.isSigmaAlgebra (d:ℕ) : (IsNull.boolean_algebra def IsNull.sigmaAlgebra (d:ℕ) : ConcreteSigmaAlgebra (EuclideanSpace' d) := (IsNull.boolean_algebra.isSigmaAlgebra d).toSigmaAlgebra -theorem JordanMeasurable.boolean_algebra.not_isSigmaAlgebra (d:ℕ) : ¬ (JordanMeasurable.boolean_algebra d).isSigmaAlgebra := +theorem JordanMeasurable.boolean_algebra.not_isSigmaAlgebra (d:ℕ) (hd: d ≥ 1) : + ¬ (JordanMeasurable.boolean_algebra d).isSigmaAlgebra := by sorry /-- Exercise 1.4.12 -/