From 89098c8f15981f48fc09c771a5087adeb775d329 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:34:48 +0530 Subject: [PATCH] Fill that the restriction of a sigma-algebra is a sigma-algebra. --- Analysis/MeasureTheory/Section_1_4_2.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_2.lean b/Analysis/MeasureTheory/Section_1_4_2.lean index 51b417363..dbaee8da3 100644 --- a/Analysis/MeasureTheory/Section_1_4_2.lean +++ b/Analysis/MeasureTheory/Section_1_4_2.lean @@ -46,7 +46,13 @@ theorem JordanMeasurable.boolean_algebra.not_isSigmaAlgebra (d:ℕ) (hd: d ≥ 1 by sorry /-- Exercise 1.4.12 -/ -theorem ConcreteSigmaAlgebra.restrict_is_sigma {X:Type*} (B: ConcreteSigmaAlgebra X) (A:Set X): (B.restrict A).isSigmaAlgebra := by sorry +theorem ConcreteSigmaAlgebra.restrict_is_sigma {X:Type*} (B: ConcreteSigmaAlgebra X) (A:Set X): (B.restrict A).isSigmaAlgebra := by + classical + intro E hE + choose E' hmeas heq using hE + refine ⟨⋃ n, E' n, B.countable_union_mem E' hmeas, ?_⟩ + ext x + simp [heq] def ConcreteSigmaAlgebra.restrict {X:Type*} (B: ConcreteSigmaAlgebra X) (A:Set X) : ConcreteSigmaAlgebra A := (B.restrict_is_sigma A).toSigmaAlgebra