From b5e18417562c7fa64e2dc032e27017edbcb3a969 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 16:27:56 +0530 Subject: [PATCH] Show the Jordan algebra contains the elementary algebra. Elementary sets are Jordan measurable, and the two algebras use the same disjunction with complements. --- Analysis/MeasureTheory/Section_1_4_1.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_4_1.lean b/Analysis/MeasureTheory/Section_1_4_1.lean index 59bee3421..9118a1e6f 100644 --- a/Analysis/MeasureTheory/Section_1_4_1.lean +++ b/Analysis/MeasureTheory/Section_1_4_1.lean @@ -72,8 +72,11 @@ def JordanMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (Euclidean } def JordanMeasurable.gt_elementary_boolean_algebra (d:ℕ) : - JordanMeasurable.boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d := - by sorry + JordanMeasurable.boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d := by + intro E hE + rcases hE with h | h + · exact Or.inl h.jordanMeasurable + · exact Or.inr h.jordanMeasurable /-- Example 1.4.5 (Lebesgue algebra) -/ def LebesgueMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=