Аналіз I, Глава 9.7

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:

namespace Chapter9

Теорема 9.7.1 (Intermediate value theorem)

theorem declaration uses 'sorry'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 := 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 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)⊢ ∃ 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 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)⊢ ∃ 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⊢ ∃ 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 = y; All goals completed! 🐙 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⊢ ∃ 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 = y; All goals completed! 🐙 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 a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhyb:¬y = f bhy_left:f a ≤ y ∧ y ≤ f bhya:y ≤ f a⊢ y = f a; 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 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:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:f b ≤ y⊢ y = f 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}⊢ ∃ c ∈ Set.Icc a b, f c = y have hE : E ⊆ 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 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:f a ≤ y ∧ y ≤ f bhya:f a < yhyb:y < f bE:Set ℝ := {x | x ∈ Set.Icc a b ∧ f x < y}x:ℝhx₁:x ∈ Set.Icc a bhx₂:f x < y⊢ x ∈ 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 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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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 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: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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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.Tendsto x Filter.atTop (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 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: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 - 0a:ℝ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 => 1 / (↑j + 1)) Filter.atTop (nhds 0) 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! 🐙 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 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: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 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: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:c = b⊢ y < f c rwa [hfc_uppera:ℝ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:c = b⊢ y < f b replace 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 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: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:b ≤ 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 Ehfc_upper:f c ≤ yhne:b ≤ chc:a ≤ c ∧ c ≤ b⊢ c = b; 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 a) (f b)⊢ ∃ 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 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: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 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 a) (f b)⊢ ∃ 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 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: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 + 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; 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 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: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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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 Ehfc_upper:f c ≤ yhne:c < bN:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bn:ℕhn:n ≥ Nthis:c + 1 / (↑n + 1) > chc:a ≤ c ∧ c ≤ b⊢ a ≤ c + 1 / (↑n + 1) 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 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: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 a) (f b)⊢ ∃ 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 a) (f b)⊢ ∃ 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 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: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 + 1 / (↑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:∀ 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 + 1 / (↑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:∀ 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:a ≤ c + 1 / (↑n + 1) ∧ c + 1 / (↑n + 1) ≤ b⊢ a ≤ c + 1 / (↑n + 1) All goals completed! 🐙 have hconv : Filter.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) Filter.atTop (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 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: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 + 0a:ℝ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⊢ Filter.Tendsto (fun k => 1 / (↑k + 1)) Filter.atTop (nhds 0) 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! 🐙 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.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) Filter.atTop (Filter.principal (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 a) (f b)⊢ ∃ 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, 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, 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! 🐙

Ремарка 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! 🐙

Ремарка 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! 🐙

Наслідок 9.7.4 (Images of continuous functions) / Вправа 9.7.1

theorem declaration uses 'sorry'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 := 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 (Set.Icc a b)) : f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.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! 🐙

Вправа 9.7.2

theorem declaration uses 'sorry'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 := 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