From 1cfefffb8509bd766cc6ded9748c478ccd6e407a Mon Sep 17 00:00:00 2001 From: Taksh Date: Fri, 14 Aug 2026 08:19:25 +0530 Subject: [PATCH] fix: scope Exercise 1.2.2's boundedness hypothesis to its own conjunct MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The statement read ∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M ∧ (pointwise convergence) ∧ (each fₙ Riemann integrable) ∧ (F not) so `∀ n, ∀ x ∈ Icc 0 1` binds the whole conjunction, not just the bound `|f n x| ≤ M`. The three later conjuncts mention neither `n` nor that `x`, so each is re-asserted once per pair -- and the `∀ n` is shadowed by the `∀ n` inside the third conjunct. Modulo `ℕ` and `Icc 0 1` being nonempty this is equivalent to the intended statement, so nothing is proved or unproved by the change; it just stops the reader having to check that equivalence to see what the exercise asks. Parenthesise the bound as its own conjunct, matching how Exercise 1.2.2' directly below already writes the same hypothesis. --- Analysis/MeasureTheory/Section_1_2_0.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Analysis/MeasureTheory/Section_1_2_0.lean b/Analysis/MeasureTheory/Section_1_2_0.lean index 93e4cfa53..a0660cbec 100644 --- a/Analysis/MeasureTheory/Section_1_2_0.lean +++ b/Analysis/MeasureTheory/Section_1_2_0.lean @@ -575,7 +575,8 @@ example : /-- Exercise 1.2.2 -/ -- The pointwise limit of uniformly bounded Riemann integrable functions need not be Riemann integrable. -example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, ∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M ∧ +example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, + (∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) ∧ (∀ x ∈ Set.Icc 0 1, Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (F x))) ∧ (∀ n, RiemannIntegrableOn (f n) (Icc 0 1)) ∧ ¬ RiemannIntegrableOn F (Icc 0 1) := by