1. Analysis
  2. 9.6. The maximum principle
Imports
import Mathlib.Tactic import Mathlib.Data.Real.Sign import Analysis.Section_9_3 import Analysis.Section_9_4

Analysis I, Section 9.6: The maximum principle

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:

  • Continuous functions on closed and bounded intervals are bounded.

  • Continuous functions on closed and bounded intervals attain their maximum and minimum.

namespace Chapter9

Definition 9.6.1

abbrev BddAboveOn (f:ℝ → ℝ) (X:Set ℝ) : Prop := ∃ M, ∀ x ∈ X, f x ≤ M
abbrev BddBelowOn (f:ℝ → ℝ) (X:Set ℝ) : Prop := ∃ M, ∀ x ∈ X, -M ≤ f xabbrev BddOn (f:ℝ → ℝ) (X:Set ℝ) : Prop := ∃ M, ∀ x ∈ X, |f x| ≤ M

Remark 9.6.2

theorem declaration uses `sorry`BddOn.iff (f:ℝ → ℝ) (X:Set ℝ) : BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X := f:ℝ → ℝX:Set ℝ⊢ BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X All goals completed! 🐙
theorem declaration uses `sorry`BddOn.iff' (f:ℝ → ℝ) (X:Set ℝ) : BddOn f X ↔ Bornology.IsBounded (f '' X) := f:ℝ → ℝX:Set ℝ⊢ BddOn f X ↔ Bornology.IsBounded (f '' X) All goals completed! 🐙theorem BddOn.of_bounded {f :ℝ → ℝ} {X: Set ℝ} {M:ℝ} (h: ∀ x ∈ X, |f x| ≤ M) : BddOn f X := f:ℝ → ℝX:Set ℝM:ℝh:∀ x ∈ X, |f x| ≤ M⊢ BddOn f X All goals completed! 🐙declaration uses `sorry`example : Continuous (fun x:ℝ ↦ x) := ⊢ Continuous fun x ↦ x All goals completed! 🐙declaration uses `sorry`example : ¬ BddOn (fun x:ℝ ↦ x) .univ := ⊢ ¬BddOn (fun x ↦ x) Set.univ All goals completed! 🐙declaration uses `sorry`example : BddOn (fun x:ℝ ↦ x) (.Icc 1 2) := ⊢ BddOn (fun x ↦ x) (Set.Icc 1 2) All goals completed! 🐙declaration uses `sorry`example : ContinuousOn (fun x:ℝ ↦ 1/x) (.Ioo 0 1) := ⊢ ContinuousOn (fun x ↦ 1 / x) (Set.Ioo 0 1) All goals completed! 🐙declaration uses `sorry`example : ¬ BddOn (fun x:ℝ ↦ 1/x) (.Ioo 0 1) := ⊢ ¬BddOn (fun x ↦ 1 / x) (Set.Ioo 0 1) All goals completed! 🐙theorem declaration uses `sorry`why_7_6_3 {n: ℕ → ℕ} (hn: StrictMono n) (j:ℕ) : n j ≥ j := n:ℕ → ℕhn:StrictMono nj:ℕ⊢ n j ≥ j All goals completed! 🐙

Lemma 9.6.3

theorem BddOn.of_continuous_on_compact {a b:ℝ} (_h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b) ) : BddOn f (.Icc a b) := a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) -- This proof is written to follow the structure of the original text. a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (M : ℝ), ∃ x ∈ Set.Icc a b, M < |f x|⊢ False; a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choose⊢ False have hx (n:ℕ) : a ≤ x n ∧ x n ≤ b ∧ n < |f (x n)| := a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosen:ℕh3:↑n < |f ⋯.choose|h1:a ≤ ⋯.chooseh2:⋯.choose ≤ b⊢ a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|; All goals completed! 🐙 a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f X⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)⊢ False have haX (n:ℕ): x n ∈ X := a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ⊢ a ≤ x n ∧ x n ≤ b; a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.chooseX:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)n:ℕhx:a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|⊢ a ≤ x n ∧ x n ≤ b; All goals completed! 🐙 a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f XhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ j⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jhf:ContinuousWithinAt f X L⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jhf:Convergesto X f (f L) L⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jhf:Filter.Tendsto (fun n_1 ↦ f (x (n n_1))) Filter.atTop (nhds (f L))⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jhf:Bornology.IsBounded (Set.range fun n_1 ↦ f (x (n n_1)))⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jhf:∃ M > 0, (Set.range fun n_1 ↦ f (x (n n_1))) ⊆ Set.Icc (-M) M⊢ False; a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jM:ℝhpos:M > 0hM:(Set.range fun n_1 ↦ f (x (n n_1))) ⊆ Set.Icc (-M) M⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jM:ℝhpos:M > 0hM:(Set.range fun n_1 ↦ f (x (n n_1))) ⊆ Set.Icc (-M) Mj:ℕhj:M < ↑j⊢ False a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.chooseX:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jM:ℝhpos:M > 0hM:(Set.range fun n_1 ↦ f (x (n n_1))) ⊆ Set.Icc (-M) Mj:ℕhj:M < ↑jhx:↑(n j) < |f (x (n j))|⊢ False replace hM : f (x (n j)) ∈ Set.Icc (-M) M := a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) All goals completed! 🐙 a:ℝb:ℝ_h:a < bf:ℝ → ℝhunbound:∀ (M : ℝ), ∃ x, (a ≤ x ∧ x ≤ b) ∧ M < |f x|x:ℕ → ℝ := fun n ↦ ⋯.chooseX:Set ℝ := Set.Icc a bhXclosed:IsClosed (Set.Icc a b)hXbounded:Bornology.IsBounded (Set.Icc a b)haX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds L)why:∀ (j : ℕ), n j ≥ jM:ℝhpos:M > 0j:ℕhj:M < ↑jhx:↑(n j) < |f (x (n j))|hM:|f (x (n j))| ≤ M⊢ False have : n j ≥ (j:ℝ) := a:ℝb:ℝ_h:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) All goals completed! 🐙 All goals completed! 🐙
/- Definition 9.6.5. Use the Mathlib `IsMaxOn` type. -/ isMaxOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} : IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a#check isMaxOn_iffisMinOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} : IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x#check isMinOn_iff
isMinOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} :
  IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x

Remark 9.6.6

theorem declaration uses `sorry`BddAboveOn.isMaxOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (h: IsMaxOn f X x₀): BddAboveOn f X := f:ℝ → ℝX:Set ℝx₀:ℝh:IsMaxOn f X x₀⊢ BddAboveOn f X All goals completed! 🐙
theorem declaration uses `sorry`BddBelowOn.isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (h: IsMinOn f X x₀): BddBelowOn f X := f:ℝ → ℝX:Set ℝx₀:ℝh:IsMinOn f X x₀⊢ BddBelowOn f X All goals completed! 🐙

Proposition 9.6.7 (Maximum principle)

theorem declaration uses `sorry`IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (.Icc a b) xmax := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax -- This proof is written to follow the structure of the original text. a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ M⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a b⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax have hE : E ⊆ .Icc (-M) M := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bx:ℝhx:x ∈ Set.Icc a b⊢ f x ∈ Set.Icc (-M) M; All goals completed! 🐙 have hnon : E ≠ ∅ := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) M⊢ ¬Set.Icc a b = ∅; a:ℝb:ℝf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mh:Set.Icc a b = ∅⊢ b ≤ a; All goals completed! 🐙 a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup E⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ m⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh✝:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mh:∃ xmax ∈ Set.Icc a b, f xmax = m⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmaxa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ m⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh✝:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mh:∃ xmax ∈ Set.Icc a b, f xmax = m⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax All goals completed! 🐙 have claim2 (n:ℕ) : ∃ x ∈ Set.Icc a b, m - 1/(n+1:ℝ) < f x := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax All goals completed! 🐙 replace : m - 1/(n+1:ℝ) < sSup E := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax All goals completed! 🐙 a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E.Nonemptym:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mn:ℕthis:m - 1 / (↑n + 1) < sSup E⊢ ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f x a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E.Nonemptym:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mn:ℕthis:∃ a ∈ E, m - 1 / (↑n + 1) < a⊢ ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f x All goals completed! 🐙 a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choose⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a b⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)⊢ ∃ xmax ∈ Set.Icc a b, f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)⊢ f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ j⊢ f xmax = m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))⊢ f xmax = m have hlower (j:ℕ) : m - 1/(j+1:ℝ) < f (x (n j)) := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))j:ℕ⊢ m - 1 / (↑j + 1) ≤ m - 1 / (↑(n j) + 1); a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))j:ℕ⊢ j ≤ n j; All goals completed! 🐙 have hupper (j:ℕ) : f (x (n j)) ≤ m := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))j:ℕ⊢ f (x (n j)) ∈ E; a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))j:ℕ⊢ ∃ x_1, (a ≤ x_1 ∧ x_1 ≤ b) ∧ f x_1 = f (x (n j)); All goals completed! 🐙 have hconvm : Filter.atTop.Tendsto (fun j ↦ f (x (n j))) (nhds m) := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ Filter.Tendsto (fun j ↦ m - 1 / (↑j + 1)) Filter.atTop (nhds m)a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ Filter.Tendsto (fun x ↦ m) Filter.atTop (nhds m)a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ (fun j ↦ m - 1 / (↑j + 1)) ≤ fun j ↦ f (x (n j))a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ (fun j ↦ f (x (n j))) ≤ fun x ↦ m a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ Filter.Tendsto (fun j ↦ m - 1 / (↑j + 1)) Filter.atTop (nhds m) a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ m = m - 0; All goals completed! 🐙 a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ Filter.Tendsto (fun x ↦ m) Filter.atTop (nhds m) All goals completed! 🐙 a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ m⊢ (fun j ↦ m - 1 / (↑j + 1)) ≤ fun j ↦ f (x (n j)) a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)M:ℝhM:∀ x ∈ Set.Icc a b, |f x| ≤ ME:Set ℝ := f '' Set.Icc a bhE:E ⊆ Set.Icc (-M) Mhnon:E ≠ ∅m:ℝ := sSup Eclaim1:∀ {y : ℝ}, y ∈ E → y ≤ mclaim2:∀ (n : ℕ), ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f xx:ℕ → ℝ := fun n ↦ ⋯.choosehx:∀ (n : ℕ), x n ∈ Set.Icc a bhfx:∀ (n : ℕ), m - 1 / (↑n + 1) < f (x n)hclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)n:ℕ → ℕhn:StrictMono nxmax:ℝhmax:xmax ∈ Set.Icc a bhconv:Filter.Tendsto (fun j ↦ x (n j)) Filter.atTop (nhds xmax)hn_lower:∀ (j : ℕ), n j ≥ jhconv':Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax))hlower:∀ (j : ℕ), m - 1 / (↑j + 1) < f (x (n j))hupper:∀ (j : ℕ), f (x (n j)) ≤ mi✝:ℕ⊢ (fun j ↦ m - 1 / (↑j + 1)) i✝ ≤ (fun j ↦ f (x (n j))) i✝; All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙
theorem declaration uses `sorry`IsMinOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) : ∃ xmin ∈ Set.Icc a b, IsMinOn f (.Icc a b) xmin := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, IsMinOn f (Set.Icc a b) xmin All goals completed! 🐙declaration uses `sorry`example : IsMaxOn (fun x ↦ x^2) (.Icc (-2) 2) 2 := ⊢ IsMaxOn (fun x ↦ x ^ 2) (Set.Icc (-2) 2) 2 All goals completed! 🐙declaration uses `sorry`example : IsMaxOn (fun x ↦ x^2) (.Icc (-2) 2) (-2) := ⊢ IsMaxOn (fun x ↦ x ^ 2) (Set.Icc (-2) 2) (-2) All goals completed! 🐙theorem sSup.of_isMaxOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMaxOn f X x₀) : sSup (f '' X) = f x₀ := f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ sSup (f '' X) = f x₀ f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ IsGreatest (f '' X) (f x₀) f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f a ≤ f x₀ All goals completed! 🐙theorem sInf.of_isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMinOn f X x₀) : sInf (f '' X) = f x₀ := f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ sInf (f '' X) = f x₀ f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ IsLeast (f '' X) (f x₀) f:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f x₀ ≤ f a All goals completed! 🐙theorem sSup.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (.Icc a b)) : ∃ xmax ∈ Set.Icc a b, sSup (f '' .Icc a b) = f xmax := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)x:ℝhx:x ∈ Set.Icc a bh':IsMaxOn f (Set.Icc a b) x⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax All goals completed! 🐙theorem sInf.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (.Icc a b)) : ∃ xmin ∈ Set.Icc a b, sInf (f '' .Icc a b) = f xmin := a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin a:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)x:ℝhx:x ∈ Set.Icc a bh':IsMinOn f (Set.Icc a b) x⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin All goals completed! 🐙/-- Exercise 9.6.1 -/ declaration uses `sorry`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₀ := ⊢ ∃ f, ContinuousOn f (Set.Ioo 1 2) ∧ BddOn f (Set.Ioo 1 2) ∧ ∃ x₀ ∈ Set.Ioo 1 2, IsMinOn f (Set.Ioo 1 2) x₀ ∧ ¬∃ x₀ ∈ Set.Ioo 1 2, IsMaxOn f (Set.Ioo 1 2) x₀ All goals completed! 🐙/-- Exercise 9.6.1 -/ declaration uses `sorry`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₀ := ⊢ ∃ f, ContinuousOn f (Set.Ioo 1 2) ∧ BddOn f (Set.Ioo 1 2) ∧ ∃ x₀ ∈ Set.Ioo 1 2, IsMaxOn f (Set.Ioo 1 2) x₀ ∧ ¬∃ x₀ ∈ Set.Ioo 1 2, IsMinOn f (Set.Ioo 1 2) x₀ All goals completed! 🐙/-- Exercise 9.6.1 -/ declaration uses `sorry`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₀ := ⊢ ∃ f, BddOn f (Set.Icc (-1) 1) ∧ ¬∃ x₀ ∈ Set.Icc (-1) 1, IsMinOn f (Set.Icc (-1) 1) x₀ ∧ ¬∃ x₀ ∈ Set.Icc (-1) 1, IsMaxOn f (Set.Icc (-1) 1) x₀ All goals completed! 🐙/-- Exercise 9.6.1 -/ declaration uses `sorry`example : ∃ f: ℝ → ℝ, ¬ BddAboveOn f (.Icc (-1) 1) ∧ ¬ BddBelowOn f (.Icc (-1) 1) := ⊢ ∃ f, ¬BddAboveOn f (Set.Icc (-1) 1) ∧ ¬BddBelowOn f (Set.Icc (-1) 1) All goals completed! 🐙end Chapter9