From 16fce238c0b6b2de048f696cae47f63634628c4d Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Fri, 6 Feb 2026 19:43:29 -0800 Subject: [PATCH] Fix typos in Theorem 6.2.11 exercise statements MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - mem_ge_inf: conclusion should be `sInf E ≤ x`, not `x ≤ sInf E` - inf_ge_upper: hypothesis should be `M ∈ lowerBounds E`, not `upperBounds E` Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_2.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/analysis/Analysis/Section_6_2.lean b/analysis/Analysis/Section_6_2.lean index b6396b98..66a71b89 100644 --- a/analysis/Analysis/Section_6_2.lean +++ b/analysis/Analysis/Section_6_2.lean @@ -168,13 +168,13 @@ example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := by sorry theorem EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := by sorry /-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/ -theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sInf E := by sorry +theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : sInf E ≤ x := by sorry /-- Theorem 6.2.11 (b) / Exercise 6.2.2 -/ theorem EReal.sup_le_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sSup E ≤ M := by sorry /-- Theorem 6.2.11 (c) / Exercise 6.2.2 -/ -theorem EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sInf E ≥ M := by sorry +theorem EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ lowerBounds E) : sInf E ≥ M := by sorry #check isLUB_iff_sSup_eq #check isGLB_iff_sInf_eq