From 38ccbd1afd193176435ac9af0445cb8f010e63fe Mon Sep 17 00:00:00 2001 From: Xiaoyun Date: Mon, 27 Apr 2026 10:27:47 +0800 Subject: [PATCH] Fix Exercise 9.8.2 IVT counterexample statements --- Analysis/Section_9_8.lean | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/Analysis/Section_9_8.lean b/Analysis/Section_9_8.lean index 1ecca6c4..a9e07765 100644 --- a/Analysis/Section_9_8.lean +++ b/Analysis/Section_9_8.lean @@ -107,13 +107,25 @@ theorem BddOn.of_antitone {a b:ℝ} {f:ℝ → ℝ} (hf: AntitoneOn f (.Icc a b) /-- Exercise 9.8.2 -/ -theorem no_strictmono_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictMonoOn f (.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by sorry - -theorem no_monotone_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: MonotoneOn f (.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by sorry - -theorem no_strictanti_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictAntiOn f (.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by sorry - -theorem no_antitone_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: AntitoneOn f (.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by sorry +theorem no_strictmono_intermediate_value : + ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictMonoOn f (.Icc a b)), + ∃ y, (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ + ¬ ∃ c ∈ Set.Icc a b, f c = y := by sorry + +theorem no_monotone_intermediate_value : + ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: MonotoneOn f (.Icc a b)), + ∃ y, (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ + ¬ ∃ c ∈ Set.Icc a b, f c = y := by sorry + +theorem no_strictanti_intermediate_value : + ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictAntiOn f (.Icc a b)), + ∃ y, (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ + ¬ ∃ c ∈ Set.Icc a b, f c = y := by sorry + +theorem no_antitone_intermediate_value : + ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: AntitoneOn f (.Icc a b)), + ∃ y, (y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) ∧ + ¬ ∃ c ∈ Set.Icc a b, f c = y := by sorry /-- Exercise 9.8.3 -/ theorem mono_of_continuous_inj {a b:ℝ} (h: a < b) {f:ℝ → ℝ}