From a4e0e4e09599349109fc8aae42cf27ec072617ae Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Tue, 10 Feb 2026 20:27:05 -0800 Subject: [PATCH] Fix ratPow_mono_of_lt_one to match Lemma 5.6.9(e) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The iff direction was wrong: for 0 < x < 1, exponentiation reverses the order. Change to rpow x q > rpow x r ↔ q < r, matching the convention in Lemma 5.6.9(e) / Exercise 5.6.2. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_7.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis/Analysis/Section_6_7.lean b/analysis/Analysis/Section_6_7.lean index b92cf82b..b225b3b8 100644 --- a/analysis/Analysis/Section_6_7.lean +++ b/analysis/Analysis/Section_6_7.lean @@ -180,7 +180,7 @@ theorem Real.ratPow_mono_of_gt_one {x:ℝ} (hx: x > 1) {q r:ℝ} : rpow x q > rp sorry /-- Proposition 6.7.3(e) / Exercise 6.7.1 -/ -theorem Real.ratPow_mono_of_lt_one {x:ℝ} (hx0: 0 < x) (hx: x < 1) {q r:ℝ} : rpow x q < rpow x r ↔ q < r := by +theorem Real.ratPow_mono_of_lt_one {x:ℝ} (hx0: 0 < x) (hx: x < 1) {q r:ℝ} : rpow x q > rpow x r ↔ q < r := by sorry /-- Proposition 6.7.3(f) / Exercise 6.7.1 -/