1. Analysis
  2. 9.7. The intermediate value theorem
Imports
import Mathlib.Tactic import Analysis.Section_9_3 import Analysis.Section_9_4

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.

namespace Chapter9

Theorem 9.7.1 (Intermediate value theorem)

theorem declaration uses `sorry`intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) {y:ℝ} (hy: y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)) : ∃ c ∈ Set.Icc a b, f c = y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y -- This proof is written to follow the structure of the original text. a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_right:y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:y = f a⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:y = f a⊢ a ∈ Set.Icc a b ∧ f a = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:y = f b⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:y = f b⊢ b ∈ Set.Icc a b ∧ f b = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhya:¬y = f ahyb:¬y = f bhy_left:f a ≤ y ∧ y ≤ f b⊢ ∃ c ∈ Set.Icc a b, f c = y replace hya : f a < y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace hyb : y < f b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a b⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove E⊢ ∃ c ∈ Set.Icc a b, f c = y have hEa : a ∈ E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have hE_nonempty : E.Nonempty := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ ∃ c ∈ Set.Icc a b, f c = y have hc : c ∈ Set.Icc a b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ a ≤ c ∧ c ≤ b; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ a ≤ ca:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ c ≤ b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ a ≤ c All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup E⊢ b = sSup (Set.Icc a b) All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a b⊢ f c = y have hfc_upper : f c ≤ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y have hxe (n:ℕ) : ∃ x ∈ E, c - 1/(n+1:ℝ) < x := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c - 1/(n+1:ℝ) < sSup E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choose⊢ f c ≤ y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ E⊢ f c ≤ y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ f c ≤ y have : Filter.atTop.Tendsto x (nhds c) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ Filter.Tendsto (fun j ↦ c - 1 / (↑j + 1)) Filter.atTop (nhds c)a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ Filter.Tendsto (fun j ↦ c) Filter.atTop (nhds c)a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ (fun j ↦ c - 1 / (↑j + 1)) ≤ xa:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ x ≤ fun j ↦ c a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ Filter.Tendsto (fun j ↦ c - 1 / (↑j + 1)) Filter.atTop (nhds c) a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ c = c - 0;All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ Filter.Tendsto (fun j ↦ c) Filter.atTop (nhds c) All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x n⊢ (fun j ↦ c - 1 / (↑j + 1)) ≤ x All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx1:∀ (n : ℕ), x n ∈ Ehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x nthis:Filter.Tendsto (fun n ↦ f (x n)) Filter.atTop (nhds (f c))⊢ f c ≤ y have hfxny (n:ℕ) : f (x n) ≤ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x nthis:Filter.Tendsto (fun n ↦ f (x n)) Filter.atTop (nhds (f c))n:ℕhx1:x n ∈ E⊢ f (x n) ≤ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhxe:∀ (n : ℕ), ∃ x ∈ E, c - 1 / (↑n + 1) < xx:ℕ → ℝ := fun n ↦ ⋯.choosehx2:∀ (n : ℕ), c - 1 / (↑n + 1) < x nthis:Filter.Tendsto (fun n ↦ f (x n)) Filter.atTop (nhds (f c))n:ℕhx1:(a ≤ x n ∧ x n ≤ b) ∧ f (x n) < y⊢ f (x n) ≤ y; All goals completed! 🐙 All goals completed! 🐙 have hne : c < b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have hfc_lower : y ≤ f c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y have : ∃ N:ℕ, ∀ n ≥ N, (c+1/(n+1:ℝ)) < b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑N⊢ ∃ N, ∀ n ≥ N, c + 1 / (↑n + 1) < b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑N⊢ ∀ n ≥ N, c + 1 / (↑n + 1) < b; intro n a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ N⊢ c + 1 / (↑n + 1) < b have hpos : 0 < b-c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have : 1/(n+1:ℝ) < b-c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 1 / (b - c) < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 0 < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 0 < b - c a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 1 / (b - c) < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 0 < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ 0 < b - c (try All goals completed! 🐙); a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ ↑N < ↑n + 1; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < b - c⊢ N < n + 1; All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < b⊢ y ≤ f c have hmem : ∀ n ≥ N, (c + 1/(n+1:ℝ)) ∈ Set.Icc a b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y intro n a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bn:ℕhn:n ≥ N⊢ c + 1 / (↑n + 1) ∈ Set.Icc a b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bn:ℕhn:n ≥ N⊢ a ≤ c + 1 / (↑n + 1) have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c + 1/(n+1:ℝ) > c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 have : ∀ n ≥ N, c + 1/(n+1:ℝ) ∉ E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y intro n a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bn:ℕa✝:n ≥ N⊢ c + 1 / (↑n + 1) ∉ E have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c + 1/(n+1:ℝ) > c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 replace : ∀ n ≥ N, f (c + 1/(n+1:ℝ)) ≥ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y intro n a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, c + 1 / (↑n + 1) ∉ En:ℕhn:n ≥ N⊢ f (c + 1 / (↑n + 1)) ≥ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bn:ℕhn:n ≥ Nthis:c + 1 / (↑n + 1) ∉ E⊢ f (c + 1 / (↑n + 1)) ≥ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bn:ℕhn:n ≥ Nthis:f (c + 1 / (↑n + 1)) < y⊢ c + 1 / (↑n + 1) ∈ E a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bn:ℕhn:n ≥ Nthis:f (c + 1 / (↑n + 1)) < y⊢ (a ≤ c + (↑n + 1)⁻¹ ∧ c + (↑n + 1)⁻¹ ≤ b) ∧ f (c + (↑n + 1)⁻¹) < y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bn:ℕhn:n ≥ Nthis✝:f (c + 1 / (↑n + 1)) < ythis:c + 1 / (↑n + 1) ∈ Set.Icc a b⊢ (a ≤ c + (↑n + 1)⁻¹ ∧ c + (↑n + 1)⁻¹ ≤ b) ∧ f (c + (↑n + 1)⁻¹) < y All goals completed! 🐙 have hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) (nhds c) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ y⊢ c = c + 0; All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhdsWithin c (Set.Icc a b)) (nhds (f c))⊢ y ≤ f c a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))⊢ y ≤ f c have hconv' : Filter.atTop.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) (.principal (.Icc a b)) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f b) (f a)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → c + 1 / (↑b_1 + 1) ∈ Set.Icc a b; All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c ⊓ Filter.principal (Set.Icc a b))⊢ y ≤ f c a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c ⊓ Filter.principal (Set.Icc a b))⊢ ∀ᶠ (c_1 : ℕ) in Filter.atTop, y ≤ (f ∘ fun n ↦ c + 1 / (↑n + 1)) c_1 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}hE:E ⊆ Set.Icc a bhE_bdd:BddAbove EhEa:a ∈ EhE_nonempty:E.Nonemptyc:ℝ := sSup Ehc:c ∈ Set.Icc a bhfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ N, c + 1 / (↑n + 1) ∈ Set.Icc a bthis:∀ n ≥ N, f (c + 1 / (↑n + 1)) ≥ yhconv:Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c)hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':Filter.Tendsto (fun n ↦ c + 1 / (↑n + 1)) Filter.atTop (nhds c ⊓ Filter.principal (Set.Icc a b))⊢ ∃ a, ∀ (b : ℕ), a ≤ b → y ≤ f (c + 1 / (↑b + 1)); All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙
open Classical in noncomputable abbrev f_9_7_1 : ℝ → ℝ := fun x ↦ if x ≤ 0 then -1 else 1declaration uses `sorry`example : 0 ∈ Set.Icc (f_9_7_1 (-1)) (f_9_7_1 1) ∧ ¬ ∃ x ∈ Set.Icc (-1) 1, f_9_7_1 x = 0 := ⊢ 0 ∈ Set.Icc (f_9_7_1 (-1)) (f_9_7_1 1) ∧ ¬∃ x ∈ Set.Icc (-1) 1, f_9_7_1 x = 0 All goals completed! 🐙

Remark 9.7.2

abbrev f_9_7_2 : ℝ → ℝ := fun x ↦ x^3 - x
declaration uses `sorry`example : f_9_7_2 (-2) = -6 := ⊢ f_9_7_2 (-2) = -6 All goals completed! 🐙declaration uses `sorry`example : f_9_7_2 2 = 6 := ⊢ f_9_7_2 2 = 6 All goals completed! 🐙declaration uses `sorry`example : f_9_7_2 (-1) = 0 := ⊢ f_9_7_2 (-1) = 0 All goals completed! 🐙declaration uses `sorry`example : f_9_7_2 0 = 0 := ⊢ f_9_7_2 0 = 0 All goals completed! 🐙declaration uses `sorry`example : f_9_7_2 1 = 0 := ⊢ f_9_7_2 1 = 0 All goals completed! 🐙/-- Remark 9.7.3 -/ declaration uses `sorry`example : ∃ x:ℝ, 0 ≤ x ∧ x ≤ 2 ∧ x^2 = 2 := ⊢ ∃ x, 0 ≤ x ∧ x ≤ 2 ∧ x ^ 2 = 2 All goals completed! 🐙

Corollary 9.7.4 (Images of continuous functions) / Exercise 9.7.1

theorem declaration uses `sorry`continuous_image_Icc {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) {y:ℝ} (hy: sInf (f '' .Icc a b) ≤ y ∧ y ≤ sSup (f '' .Icc a b)) : ∃ c ∈ Set.Icc a b, f c = y := a:ℝb:ℝhab:a < bf:ℝ → ℝ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 All goals completed! 🐙
theorem declaration uses `sorry`continuous_image_Icc' {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) : f '' .Icc a b = .Icc (sInf (f '' .Icc a b)) (sSup (f '' .Icc a b)) := a:ℝb:ℝhab:a < bf:ℝ → ℝ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)) All goals completed! 🐙

Exercise 9.7.2

theorem declaration uses `sorry`exists_fixed_pt {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc 0 1)) (hmap: f '' .Icc 0 1 ⊆ .Icc 0 1) : ∃ x ∈ Set.Icc 0 1, f x = x := 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 All goals completed! 🐙
end Chapter9