From 09c16f498485511927ac051ce6c5ca6acd77eae4 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 7 Sep 2026 17:36:53 +0530 Subject: [PATCH] Fill finite unions in the null-set boolean algebra. --- Analysis/MeasureTheory/Section_1_4_1.lean | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_4_1.lean b/Analysis/MeasureTheory/Section_1_4_1.lean index 59bee3421..4a611c78f 100644 --- a/Analysis/MeasureTheory/Section_1_4_1.lean +++ b/Analysis/MeasureTheory/Section_1_4_1.lean @@ -94,7 +94,24 @@ def IsNull.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) measurable := fun E => IsNull E ∨ IsNull Eᶜ empty_mem := by sorry compl_mem := by sorry - union_mem := by sorry + union_mem := fun E F hE hF => by + rcases hE with hE | hE <;> rcases hF with hF | hF + · refine Or.inl ?_ + have hle : Lebesgue_outer_measure (E ∪ F) ≤ + Lebesgue_outer_measure E + Lebesgue_outer_measure F := by + simpa [Fin.sum_univ_two] using + Lebesgue_outer_measure.finite_union_le (fun i : Fin 2 => if i = 0 then E else F) + simp [hE, hF] at hle + exact le_antisymm hle (Lebesgue_outer_measure.nonneg _) + · refine Or.inr (IsNull.subset hF ?_) + intro x hx + exact hx.2 + · refine Or.inr (IsNull.subset hE ?_) + intro x hx + exact hx.1 + · refine Or.inr (IsNull.subset hE ?_) + intro x hx + exact hx.1 } def IsNull.lt_lebesgue_boolean_algebra (d:ℕ) :