From 38ab9a37b88f4979c9b0823effe1d63625108003 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 5 Aug 2026 17:00:19 +0530 Subject: [PATCH] fix: part-label Example 5.2.2 Verso docstrings Disambiguate the three Example 5.2.2 statements for Verso. --- Analysis/Section_5_2.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Analysis/Section_5_2.lean b/Analysis/Section_5_2.lean index 75f6762a7..df10bff3f 100644 --- a/Analysis/Section_5_2.lean +++ b/Analysis/Section_5_2.lean @@ -36,14 +36,14 @@ namespace Chapter5 lemma Rat.closeSeq_def (ε: ℚ) (a b: Sequence) : ε.CloseSeq a b ↔ ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.Close (a n) (b n) := by rfl -/-- Example 5.2.2 -/ +/-- Example 5.2.2 (a) -/ example : (0.1:ℚ).CloseSeq ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence) ((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by sorry -/-- Example 5.2.2 -/ +/-- Example 5.2.2 (b) -/ example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence) := by sorry -/-- Example 5.2.2 -/ +/-- 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) -/