From f9e24af544ec00cd38d66c16428badf8afcae93d Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 19 Apr 2026 15:26:04 -0700 Subject: [PATCH] Section 9.6: fix Exercise 9.6.1 statements and add Exercise 9.6.2 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Exercise 9.6.1 c): add parens around the two ¬ ∃ conjuncts (without them, ∧ associates inside the inner ¬ ∃ body, changing the meaning). - Exercise 9.6.1 b): change domain from (1, 2) to [0, ∞), matching the textbook's unbounded-domain counterexample. - Split Exercise 9.6.1 docstring labels into a) / b) / c) / d). - Add Exercise 9.6.2: BddOn.add, BddOn.sub, BddOn.mul, and BddOn.div (the last as a Decidable, since divisibility of the bounded class is the actual question). Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_9_6.lean | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) diff --git a/Analysis/Section_9_6.lean b/Analysis/Section_9_6.lean index 097560fb..9d87f317 100644 --- a/Analysis/Section_9_6.lean +++ b/Analysis/Section_9_6.lean @@ -154,26 +154,40 @@ theorem sInf.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: C choose x hx h' using IsMinOn.of_continuous_on_compact h hf grind [sInf.of_isMinOn] -/-- Exercise 9.6.1 -/ +/-- Exercise 9.6.1 a) -/ example : ∃ f: ℝ → ℝ, ContinuousOn f (.Ioo 1 2) ∧ BddOn f (.Ioo 1 2) ∧ ∃ x₀ ∈ Set.Ioo 1 2, IsMinOn f (.Ioo 1 2) x₀ ∧ ¬ ∃ x₀ ∈ Set.Ioo 1 2, IsMaxOn f (.Ioo 1 2) x₀ := by sorry -/-- Exercise 9.6.1 -/ -example : ∃ f: ℝ → ℝ, ContinuousOn f (.Ioo 1 2) ∧ BddOn f (.Ioo 1 2) ∧ - ∃ x₀ ∈ Set.Ioo 1 2, IsMaxOn f (.Ioo 1 2) x₀ ∧ - ¬ ∃ x₀ ∈ Set.Ioo 1 2, IsMinOn f (.Ioo 1 2) x₀ +/-- Exercise 9.6.1 b) -/ +example : ∃ f: ℝ → ℝ, ContinuousOn f (.Ici 0) ∧ BddOn f (.Ici 0) ∧ + ∃ x₀ ∈ Set.Ici 0, IsMaxOn f (.Ici 0) x₀ ∧ + ¬ ∃ x₀ ∈ Set.Ici 0, IsMinOn f (.Ici 0) x₀ := by sorry -/-- Exercise 9.6.1 -/ +/-- Exercise 9.6.1 c) -/ example : ∃ f: ℝ → ℝ, BddOn f (.Icc (-1) 1) ∧ - ¬ ∃ x₀ ∈ Set.Icc (-1) 1, IsMinOn f (.Icc (-1) 1) x₀ ∧ - ¬ ∃ x₀ ∈ Set.Icc (-1) 1, IsMaxOn f (.Icc (-1) 1) x₀ + (¬ ∃ x₀ ∈ Set.Icc (-1) 1, IsMinOn f (.Icc (-1) 1) x₀) ∧ + (¬ ∃ x₀ ∈ Set.Icc (-1) 1, IsMaxOn f (.Icc (-1) 1) x₀) := by sorry -/-- Exercise 9.6.1 -/ +/-- Exercise 9.6.1 d) -/ example : ∃ f: ℝ → ℝ, ¬ BddAboveOn f (.Icc (-1) 1) ∧ ¬ BddBelowOn f (.Icc (-1) 1) := by sorry +/-- Exercise 9.6.2 -/ +theorem BddOn.add (f g : ℝ → ℝ) (X : Set ℝ) (hf : BddOn f X) (hg : BddOn g X) : + BddOn (f + g) X := by sorry + +theorem BddOn.sub (f g : ℝ → ℝ) (X : Set ℝ) (hf : BddOn f X) (hg : BddOn g X) : + BddOn (f - g) X := by sorry + +theorem BddOn.mul (f g : ℝ → ℝ) (X : Set ℝ) (hf : BddOn f X) (hg : BddOn g X) : + BddOn (f * g) X := by sorry + +def BddOn.div : Decidable (∀ (f g : ℝ → ℝ) (X : Set ℝ) (_ : ∀ x ∈ X, g x ≠ 0) (_ : BddOn f X) + (_: BddOn g X), (BddOn (f / g) X)) := by + -- the first line of this construction should be either `apply isTrue` or `apply isFalse`, depending on whether you believe the given statement to be true or false. + sorry end Chapter9