From f3743a9c67ed02c3f8db66e88fff6ed9cc28bc5d Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 15 Aug 2026 09:14:33 +0530 Subject: [PATCH 1/2] fix: disambiguate remaining duplicate Verso labels in Chapters 2, 5 and 9 Twenty-one docstrings across nine groups shared a label with a sibling: Proposition 2.1.16, Proposition 2.3.6, Definition 2.3.11, Example 5.1.10, Definition 5.1.12, Definitions 5.2.3 and 5.2.6, the Example 5.5.2 API, and Examples 9.3.4 and 9.3.5. Definitions and propositions name the case in the parenthetical; the examples take part letters. --- Analysis/Section_2_1.lean | 4 ++-- Analysis/Section_2_3.lean | 6 +++--- Analysis/Section_5_1.lean | 8 ++++---- Analysis/Section_5_2.lean | 8 ++++---- Analysis/Section_5_5.lean | 4 ++-- Analysis/Section_9_3.lean | 8 ++++---- 6 files changed, 19 insertions(+), 19 deletions(-) diff --git a/Analysis/Section_2_1.lean b/Analysis/Section_2_1.lean index 1472acab1..fd9ea507b 100644 --- a/Analysis/Section_2_1.lean +++ b/Analysis/Section_2_1.lean @@ -137,7 +137,7 @@ theorem Nat.recurse_zero (f: Nat → Nat → Nat) (c: Nat) : Nat.recurse f c 0 = theorem Nat.recurse_succ (f: Nat → Nat → Nat) (c: Nat) (n: Nat) : recurse f c (n++) = f n (recurse f c n) := by rfl -/-- Proposition 2.1.16 (recursive definitions). -/ +/-- Proposition 2.1.16 (recursive definitions, existence). -/ theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) : (a 0 = c ∧ ∀ n, a (n++) = f n (a n)) ↔ a = recurse f c := by constructor @@ -154,7 +154,7 @@ theorem Nat.eq_recurse (f: Nat → Nat → Nat) (c: Nat) (a: Nat → Nat) : exact recurse_succ _ _ -/-- Proposition 2.1.16 (recursive definitions). -/ +/-- Proposition 2.1.16 (recursive definitions, uniqueness). -/ theorem Nat.recurse_uniq (f: Nat → Nat → Nat) (c: Nat) : ∃! (a: Nat → Nat), a 0 = c ∧ ∀ n, a (n++) = f n (a n) := by apply ExistsUnique.intro (recurse f c) diff --git a/Analysis/Section_2_3.lean b/Analysis/Section_2_3.lean index 51017219c..06fd6e2c6 100644 --- a/Analysis/Section_2_3.lean +++ b/Analysis/Section_2_3.lean @@ -136,7 +136,7 @@ theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.IsPos) : a * rw [lt_iff_add_pos] use d*c -/-- Proposition 2.3.6 (Multiplication preserves order) -/ +/-- Proposition 2.3.6 (Multiplication preserves order, on the right) -/ theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.IsPos) : a * c > b * c := mul_lt_mul_of_pos_right h hc @@ -146,7 +146,7 @@ theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.IsPos) : c * a simp [mul_comm] exact mul_lt_mul_of_pos_right h hc -/-- Proposition 2.3.6 (Multiplication preserves order) -/ +/-- Proposition 2.3.6 (Multiplication preserves order, on the left) -/ theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.IsPos) : c * a > c * b := mul_lt_mul_of_pos_left h hc @@ -195,7 +195,7 @@ Compare with Mathlib's {name}`Nat.pow_zero` -/ @[simp] theorem Nat.pow_zero (m: Nat) : m ^ (0:Nat) = 1 := recurse_zero (fun _ prod ↦ prod * m) _ -/-- Definition 2.3.11 (Exponentiation for natural numbers) -/ +/-- Definition 2.3.11 (Exponentiation for natural numbers, successor) -/ @[simp] theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _ diff --git a/Analysis/Section_5_1.lean b/Analysis/Section_5_1.lean index 1f34c614b..bbe889a54 100644 --- a/Analysis/Section_5_1.lean +++ b/Analysis/Section_5_1.lean @@ -299,12 +299,12 @@ lemma Sequence.IsCauchy.mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℚ) : noncomputable def Sequence.sqrt_two : Sequence := (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ)) /-- - Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.) + Example 5.1.10 (a). (This requires extensive familiarity with Mathlib's API for the real numbers.) -/ theorem Sequence.ex_5_1_10_a : (1:ℚ).Steady sqrt_two := by sorry /-- - Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.) + Example 5.1.10 (b). (This requires extensive familiarity with Mathlib's API for the real numbers.) -/ theorem Sequence.ex_5_1_10_b : (0.1:ℚ).Steady (sqrt_two.from 1) := by sorry @@ -354,12 +354,12 @@ lemma boundedBy_def {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : BoundedBy a M ↔ ∀ i abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop := ∀ n, |a n| ≤ M -/-- Definition 5.1.12 (bounded sequences) -/ +/-- Definition 5.1.12 (bounded sequences, bounded by a given constant) -/ lemma Sequence.boundedBy_def (a:Sequence) (M:ℚ) : a.BoundedBy M ↔ ∀ n, |a n| ≤ M := by rfl abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M -/-- Definition 5.1.12 (bounded sequences) -/ +/-- Definition 5.1.12 (bounded sequences, bounded) -/ lemma Sequence.isBounded_def (a:Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M := by rfl /-- Example 5.1.13 (a) -/ diff --git a/Analysis/Section_5_2.lean b/Analysis/Section_5_2.lean index df10bff3f..2c042c013 100644 --- a/Analysis/Section_5_2.lean +++ b/Analysis/Section_5_2.lean @@ -46,11 +46,11 @@ example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence) := by sorr /-- Example 5.2.2 (c) -/ example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by sorry -/-- Definition 5.2.3 (Eventually ε-close sequences) -/ +/-- Definition 5.2.3 (Eventually ε-close sequences, unfolded) -/ lemma Rat.eventuallyClose_def (ε: ℚ) (a b: Sequence) : ε.EventuallyClose a b ↔ ∃ N, ε.CloseSeq (a.from N) (b.from N) := by rfl -/-- Definition 5.2.3 (Eventually ε-close sequences) -/ +/-- Definition 5.2.3 (Eventually ε-close sequences, in terms of the terms) -/ lemma Rat.eventuallyClose_iff (ε: ℚ) (a b: ℕ → ℚ) : ε.EventuallyClose (a:Sequence) (b:Sequence) ↔ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := by sorry @@ -68,11 +68,11 @@ example : (0.01:ℚ).EventuallyClose ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Se abbrev Sequence.Equiv (a b: ℕ → ℚ) : Prop := ∀ ε > (0:ℚ), ε.EventuallyClose (a:Sequence) (b:Sequence) -/-- Definition 5.2.6 (Equivalent sequences) -/ +/-- Definition 5.2.6 (Equivalent sequences, unfolded) -/ lemma Sequence.equiv_def (a b: ℕ → ℚ) : Equiv a b ↔ ∀ (ε:ℚ), ε > 0 → ε.EventuallyClose (a:Sequence) (b:Sequence) := by rfl -/-- Definition 5.2.6 (Equivalent sequences) -/ +/-- Definition 5.2.6 (Equivalent sequences, in terms of the terms) -/ lemma Sequence.equiv_iff (a b: ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := by sorry diff --git a/Analysis/Section_5_5.lean b/Analysis/Section_5_5.lean index 2861a06a8..fbcd4b5d7 100644 --- a/Analysis/Section_5_5.lean +++ b/Analysis/Section_5_5.lean @@ -32,10 +32,10 @@ theorem Real.upperBound_def (E: Set Real) (M: Real) : M ∈ upperBounds E ↔ theorem Real.lowerBound_def (E: Set Real) (M: Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M := mem_lowerBounds -/-- API for Example 5.5.2 -/ +/-- API for Example 5.5.2 (the interval) -/ theorem Real.Icc_def (x y:Real) : .Icc x y = { z | x ≤ z ∧ z ≤ y } := rfl -/-- API for Example 5.5.2 -/ +/-- API for Example 5.5.2 (membership) -/ theorem Real.mem_Icc (x y z:Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y := by simp [Real.Icc_def] /-- Example 5.5.2 -/ diff --git a/Analysis/Section_9_3.lean b/Analysis/Section_9_3.lean index 2e8af602c..ec9c1ad56 100644 --- a/Analysis/Section_9_3.lean +++ b/Analysis/Section_9_3.lean @@ -49,19 +49,19 @@ Slight change from the book to accomodate the change to {lean}`Real.CloseFn` -/ example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry -/-- Example 9.3.4 -/ +/-- Example 9.3.4 (a) -/ example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry -/-- Example 9.3.4 -/ +/-- Example 9.3.4 (b) -/ example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := by sorry -/-- Example 9.3.5 -/ +/-- Example 9.3.5 (a) -/ example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := by sorry -/-- Example 9.3.5 -/ +/-- Example 9.3.5 (b) -/ example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := by sorry From a8fc2e7d177eddeea187336d40de24a7c2e7040a Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 24 Aug 2026 21:05:26 +0530 Subject: [PATCH 2/2] fix: use descriptive parentheticals for Examples 9.3.4 and 9.3.5 labels Both are single-paragraph example environments in ch9 with no enumerated parts, so (a)/(b) pointed at parts a reader cannot find. Describe the two cases instead, matching the style used elsewhere in this PR. --- Analysis/Section_9_3.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Analysis/Section_9_3.lean b/Analysis/Section_9_3.lean index ec9c1ad56..a65697835 100644 --- a/Analysis/Section_9_3.lean +++ b/Analysis/Section_9_3.lean @@ -49,19 +49,19 @@ Slight change from the book to accomodate the change to {lean}`Real.CloseFn` -/ example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry -/-- Example 9.3.4 (a) -/ +/-- Example 9.3.4 (not close on the whole interval) -/ example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry -/-- Example 9.3.4 (b) -/ +/-- Example 9.3.4 (close near the point) -/ example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 4 2 := by sorry -/-- Example 9.3.5 (a) -/ +/-- Example 9.3.5 (not close on the whole interval) -/ example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 9 := by sorry -/-- Example 9.3.5 (b) -/ +/-- Example 9.3.5 (close near the point) -/ example: (0.1:ℝ).CloseNear (.Icc 1 3) (fun x ↦ x^2) 9 3 := by sorry