From 08406b8ce138b4f1f1fd920d09137b9bcfbd3e5b Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Mon, 3 Aug 2026 14:44:19 +0530
Subject: [PATCH 1/2] =?UTF-8?q?fix:=20label=20Ex.=201.2.2=20(i)/(ii)=20and?=
 =?UTF-8?q?=20Ex.=209.2.1=20(a)=E2=80=93(d)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Drop the 1.2.22 hunk — already disambiguated on main. Keep the missing
9.2.1 (c)/(d) Verso docs Tao asked for.
---
 Analysis/MeasureTheory/Section_1_2_0.lean | 4 ++--
 Analysis/Section_9_2.lean                 | 6 ++++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/Analysis/MeasureTheory/Section_1_2_0.lean b/Analysis/MeasureTheory/Section_1_2_0.lean
index f61b9aae4..4806a8bab 100644
--- a/Analysis/MeasureTheory/Section_1_2_0.lean
+++ b/Analysis/MeasureTheory/Section_1_2_0.lean
@@ -573,7 +573,7 @@ example :
 
 
 
-/-- Exercise 1.2.2 -/
+/-- Exercise 1.2.2 (i) -/
 -- 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 ∧
     (∀ x ∈ Set.Icc 0 1, Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (F x))) ∧
@@ -581,7 +581,7 @@ example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, ∃ M, ∀ n, ∀ x 
     ¬ RiemannIntegrableOn F (Icc 0 1) := by
   sorry
 
-/-- Exercise 1.2.2 -/
+/-- Exercise 1.2.2 (ii) -/
 -- Determine whether uniform convergence of uniformly bounded Riemann integrable functions preserves Riemann integrability (true or false).
 def Ex_1_2_2b : Decidable ( ∀ f: ℕ → ℝ → ℝ, ∀ F: ℝ → ℝ, (∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) → (∀ x ∈ Set.Icc 0 1, TendstoUniformly f F Filter.atTop) → (∀ n, RiemannIntegrableOn (f n) (Icc 0 1)) → RiemannIntegrableOn F (Icc 0 1) ) := by
   -- the first line of this construction should be either `apply isTrue` or `apply isFalse`, depending on whether you believe the given statement to be true or false.
diff --git a/Analysis/Section_9_2.lean b/Analysis/Section_9_2.lean
index dda4c38e4..d96d8a1db 100644
--- a/Analysis/Section_9_2.lean
+++ b/Analysis/Section_9_2.lean
@@ -51,20 +51,22 @@ example : f_9_2_2 ∘ g_9_2_2 = fun x ↦ 4*x^2 := by grind
 
 example : g_9_2_2 ∘ f_9_2_2 = fun x ↦ 2*x^2 := by grind
 
-/-- Exercise 9.2.1. -/
+/-- Exercise 9.2.1 (a) -/
 def Exercise_9_2_1a : Decidable (∀ (f g h : ℝ → ℝ), (f+g) ∘ h = f ∘ h + g ∘ h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry
 
-/-- Exercise 9.2.1. -/
+/-- Exercise 9.2.1 (b) -/
 def Exercise_9_2_1b : Decidable (∀ (f g h : ℝ → ℝ), f ∘ (g + h) = f ∘ g + f ∘ h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry
 
+/-- Exercise 9.2.1 (c) -/
 def Exercise_9_2_1c : Decidable (∀ (f g h : ℝ → ℝ), (f+g) * h = f * h + g * h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry
 
+/-- Exercise 9.2.1 (d) -/
 def Exercise_9_2_1d : Decidable (∀ (f g h : ℝ → ℝ), f * (g+h) = f * g + f * h) := by
   -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
   sorry

From 615ac74ccee4c926101d7558445ce1da093e07f8 Mon Sep 17 00:00:00 2001
From: Taksh <takshkothari09@gmail.com>
Date: Mon, 3 Aug 2026 21:54:40 +0530
Subject: [PATCH 2/2] fix: label Ex. 1.2.2' instead of inventing (i)/(ii)

Text has two questions in one exercise; follow the primed-variant
convention from 7a9e513. Leave 1.2.22 to #632.
---
 Analysis/MeasureTheory/Section_1_2_0.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Analysis/MeasureTheory/Section_1_2_0.lean b/Analysis/MeasureTheory/Section_1_2_0.lean
index 4806a8bab..93e4cfa53 100644
--- a/Analysis/MeasureTheory/Section_1_2_0.lean
+++ b/Analysis/MeasureTheory/Section_1_2_0.lean
@@ -573,7 +573,7 @@ example :
 
 
 
-/-- Exercise 1.2.2 (i) -/
+/-- 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 ∧
     (∀ x ∈ Set.Icc 0 1, Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (F x))) ∧
@@ -581,7 +581,7 @@ example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, ∃ M, ∀ n, ∀ x 
     ¬ RiemannIntegrableOn F (Icc 0 1) := by
   sorry
 
-/-- Exercise 1.2.2 (ii) -/
+/-- Exercise 1.2.2' -/
 -- Determine whether uniform convergence of uniformly bounded Riemann integrable functions preserves Riemann integrability (true or false).
 def Ex_1_2_2b : Decidable ( ∀ f: ℕ → ℝ → ℝ, ∀ F: ℝ → ℝ, (∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) → (∀ x ∈ Set.Icc 0 1, TendstoUniformly f F Filter.atTop) → (∀ n, RiemannIntegrableOn (f n) (Icc 0 1)) → RiemannIntegrableOn F (Icc 0 1) ) := by
   -- the first line of this construction should be either `apply isTrue` or `apply isFalse`, depending on whether you believe the given statement to be true or false.