From 9c32a5286d3a3eb7db6370bf9bd857e05ce4c6ed Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:35:10 +0530 Subject: [PATCH] Show the generated boolean algebra sits inside the generated sigma-algebra. --- Analysis/MeasureTheory/Section_1_4_2.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean index 51b417363..ca7d9c6a9 100644 --- a/Analysis/MeasureTheory/Section_1_4_2.lean +++ b/Analysis/MeasureTheory/Section_1_4_2.lean @@ -122,7 +122,9 @@ instance ConcreteSigmaAlgebra.instCompleteLattice {X:Type*} : CompleteLattice (C isGLB_sInf := sorry } -theorem ConcreteSigmaAlgebra.generated_by_le {X:Type*} (F: Set (Set X)) : ConcreteBooleanAlgebra.generated_by F ≤ (ConcreteSigmaAlgebra.generated_by F).toConcreteBooleanAlgebra := by sorry +theorem ConcreteSigmaAlgebra.generated_by_le {X:Type*} (F: Set (Set X)) : ConcreteBooleanAlgebra.generated_by F ≤ (ConcreteSigmaAlgebra.generated_by F).toConcreteBooleanAlgebra := by + intro E hE B hB + exact hE B.toConcreteBooleanAlgebra fun A hA => hB A hA example : ∃ (X:Type*) (F: Set (Set X)), ConcreteBooleanAlgebra.generated_by F ≠ (ConcreteSigmaAlgebra.generated_by F).toConcreteBooleanAlgebra := by sorry