Analysis I, Section 9.7: The intermediate value theorem

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• The intermediate value theorem.

theorem Chapter9.intermediate_value {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) {y : ℝ} (hy : y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)) : ∃ c ∈ Set.Icc a b, f c = y

Theorem 9.7.1 (Intermediate value theorem)

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_7_1 : ℝ → ℝ

Equations

• Chapter9.f_9_7_1 x = if x ≤ 0 then -1 else 1

@[reducible, inline]

abbrev Chapter9.f_9_7_2 : ℝ → ℝ

Remark 9.7.2

Equations

• Chapter9.f_9_7_2 x = x ^ 3 - x

theorem Chapter9.continuous_image_Icc {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) {y : ℝ} (hy : sInf (f '' Set.Icc a b) ≤ y ∧ y ≤ sSup (f '' Set.Icc a b)) : ∃ c ∈ Set.Icc a b, f c = y

Corollary 9.7.4 (Images of continuous functions) / Exercise 9.7.1

theorem Chapter9.continuous_image_Icc' {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))

theorem Chapter9.exists_fixed_pt {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc 0 1)) (hmap : f '' Set.Icc 0 1 ⊆ Set.Icc 0 1) : ∃ x ∈ Set.Icc 0 1, f x = x

Exercise 9.7.2