From ec42ecb627f3ad9e8c3b8e8c6e161ec3b870addf Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 8 Feb 2026 16:47:53 -0800 Subject: [PATCH] Fix Exercise 6.4.6 statement: sup is not strictly monotone MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The exercise asks to show that sup is not strictly monotone, i.e., ∃ a b, (∀ n, a n < b n) ∧ ¬ a.sup < b.sup. The previous statement used ≠ instead of ¬ ... <. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_4.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean index 360cdfc9..8bff023a 100644 --- a/analysis/Analysis/Section_6_4.lean +++ b/analysis/Analysis/Section_6_4.lean @@ -299,7 +299,7 @@ theorem Sequence.Cauchy_iff_convergent (a:Sequence) : grind /-- Exercise 6.4.6 -/ -theorem Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ (a:Sequence).sup ≠ (b:Sequence).sup := by +theorem Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ ¬ (a:Sequence).sup < (b:Sequence).sup := by sorry /- Exercise 6.4.7 -/