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

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

Визначення 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 x

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

Ремарка 9.6.2

theorem declaration uses 'sorry'BddOn.iff (f:ℝ → ℝ) (X:Set ℝ) :
  BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X := byf:ℝ → ℝX:Set ℝ⊢ BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'BddOn.iff' (f:ℝ → ℝ) (X:Set ℝ) :
  BddOn f X ↔ Bornology.IsBounded (f '' X) := byf:ℝ → ℝX:Set ℝ⊢ BddOn f X ↔ Bornology.IsBounded (f '' X)
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ x) := by⊢ Continuous fun x => x sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ BddOn (fun x:ℝ ↦ x) Set.univ  := by⊢ ¬BddOn (fun x => x) Set.univ sorryAll goals completed! 🐙

declaration uses 'sorry'example : BddOn (fun x:ℝ ↦ x) (Set.Icc 1 2) := by⊢ BddOn (fun x => x) (Set.Icc 1 2) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ContinuousOn (fun x:ℝ ↦ 1/x) (Set.Ioo 0 1) := by⊢ ContinuousOn (fun x => 1 / x) (Set.Ioo 0 1) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ BddOn (fun x:ℝ ↦ 1/x) (Set.Ioo 0 1) := by⊢ ¬BddOn (fun x => 1 / x) (Set.Ioo 0 1) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'why_7_6_3 {n: ℕ → ℕ} (hn: StrictMono n) (j:ℕ) : n j ≥ j := byn:ℕ → ℕhn:StrictMono nj:ℕ⊢ n j ≥ j sorryAll goals completed! 🐙

Лема 7.6.3

theorem BddOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (Set.Icc a b) ) :
  BddOn f (Set.Icc a b) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b)
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  by_contra! hunbounda:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:¬BddOn f (Set.Icc a b)⊢ False
  simp [BddOn] at hunbounda:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|⊢ False
  set x := fun (n:ℕ) ↦ (hunbound n).choosea:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choose⊢ False
  have hx (n:ℕ) : a ≤ x n ∧ x n ≤ b ∧ n < |f (x n)| := (hunbound n).choose_speca:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|⊢ False
  set X := Set.Icc a ba:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|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
  have hXclosed : IsClosed X := Icc_closed (bya:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhf:ContinuousOn f X⊢ a ≤ b linarithAll goals completed! 🐙)
  have hXbounded : Bornology.IsBounded X := Icc_bounded _ _a:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|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 XhXbounded:Bornology.IsBounded X⊢ False
  have haX (n:ℕ): x n ∈ X := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) simp [X]a:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|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 XhXbounded:Bornology.IsBounded Xn:ℕ⊢ a ≤ x n ∧ x n ≤ b; exact ⟨ (hx n).1, (hx n).2.1 ⟩All goals completed! 🐙
  obtain ⟨ n, hn, ⟨ L, hLX, hconv ⟩ ⟩ := ((Heine_Borel X).mp ⟨ hXclosed, hXbounded ⟩) x haXintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|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 XhXbounded:Bornology.IsBounded XhaX:∀ (n : ℕ), x n ∈ Xn:ℕ → ℕhn:StrictMono nL:ℝhLX:L ∈ Xhconv:Filter.Tendsto (fun j => x (n j)) Filter.atTop (nhds L)⊢ False
  have why (j:ℕ) : n j ≥ j := why_7_6_3 hn jintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|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 XhXbounded:Bornology.IsBounded XhaX:∀ (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
  replace hf := ContinuousOn.continuousWithinAt hf hLXintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  rw [ContinuousWithinAt.iff] at hfintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  replace hf := Convergesto.comp (AdherentPt.of_mem hLX) hf (fun j ↦ haX (n j)) hconvintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  replace hf := Metric.isBounded_range_of_tendsto _ hfintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  rw [isBounded_def] at hfintro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  obtain ⟨ M, hpos, hM ⟩ := hfintro.intro.intro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  obtain ⟨ j, hj ⟩ := exists_nat_gt Mintro.intro.intro.intro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.choosehx:∀ (n : ℕ), a ≤ x n ∧ x n ≤ b ∧ ↑n < |f (x n)|X:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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
  replace hx := (hx (n j)).2.2intro.intro.intro.intro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.chooseX:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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 := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b)
    apply hMaa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.chooseX:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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))|⊢ f (x (n j)) ∈ Set.range fun n_1 => f (x (n n_1)); simpAll goals completed! 🐙
  simp [←abs_le] at hMintro.intro.intro.intro.intro.intro.introa:ℝb:ℝh:a < bf:ℝ → ℝhunbound:∀ (x : ℝ), ∃ x_1, a ≤ x_1 ∧ x_1 ≤ b ∧ x < |f x_1|x:ℕ → ℝ := fun n => ⋯.chooseX:Set ℝ := Set.Icc a bhXclosed:IsClosed XhXbounded:Bornology.IsBounded XhaX:∀ (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:ℝ) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ BddOn f (Set.Icc a b) simp [why j]All goals completed! 🐙
  linarithAll 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_iff

isMaxOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} :
  IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a

isMinOn_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

Ремарка 9.6.6

theorem declaration uses 'sorry'BddAboveOn.isMaxOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (h: IsMaxOn f X x₀): BddAboveOn f X := byf:ℝ → ℝX:Set ℝx₀:ℝh:IsMaxOn f X x₀⊢ BddAboveOn f X sorryAll goals completed! 🐙

theorem declaration uses 'sorry'BddBelowOn.isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (h: IsMinOn f X x₀): BddBelowOn f X := byf:ℝ → ℝX:Set ℝx₀:ℝh:IsMinOn f X x₀⊢ BddBelowOn f X sorryAll goals completed! 🐙

Твердження 9.6.7 (Maximum principle)

theorem declaration uses 'sorry'IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (Set.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  have hbound := BddOn.of_continuous_on_compact h hfa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hbound:BddOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
  obtain ⟨ M, hM ⟩ := hboundintroa:ℝ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
  set E := f '' (Set.Icc a b)introa:ℝ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 ⊆ Set.Icc (-M) M := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
    rintro _ ⟨ x, hx, rfl ⟩intro.introa:ℝ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
    simp [hM x hx, ←abs_le]All goals completed! 🐙
  have hnon : E ≠ ∅ := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
    simp [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) M⊢ ¬Set.Icc a b = ∅
    contrapose! ha:ℝ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
    rw [Set.Icc_eq_empty_iff] at ha:ℝ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:¬a ≤ b⊢ b ≤ a
    linarithAll goals completed! 🐙
  set m := sSup Eintroa:ℝ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
  have claim1 {y:ℝ} (hy: y ∈ E) : y ≤ m :=
    le_csSup (BddAbove.mono hE bddAbove_Icc) hyintroa:ℝ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
  suffices h : ∃ xmax, xmax ∈ Set.Icc a b ∧ f xmax = mintroa:ℝ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) xmaxha:ℝ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
  .introa:ℝ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 sorryAll goals completed! 🐙
  have claim2 (n:ℕ) : ∃ x ∈ Set.Icc a b, m - 1/(n+1:ℝ) < f x := bya:ℝ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 := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax positivityAll goals completed! 🐙
    replace : m - 1/(n+1:ℝ) < sSup E := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax linarithAll goals completed! 🐙
    rw [←Set.nonempty_iff_ne_empty] at hnona:ℝ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
    replace := exists_lt_of_lt_csSup hnon thisa:ℝ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
    simp only [Set.mem_image, exists_exists_and_eq_and, E] at thisa:ℝ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_1 ∈ Set.Icc a b, m - 1 / (↑n + 1) < f a_1⊢ ∃ x ∈ Set.Icc a b, m - 1 / (↑n + 1) < f x
    exact thisAll goals completed! 🐙
  set x : ℕ → ℝ := fun n ↦ (claim2 n).chooseha:ℝ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
  have hx (n:ℕ) : x n ∈ Set.Icc a b := (claim2 n).choose_spec.1ha:ℝ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
  have hfx (n:ℕ) : m - 1/(n+1:ℝ) < f (x n) := (claim2 n).choose_spec.2ha:ℝ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
  have hclosed : IsClosed (Set.Icc a b) := Icc_closed (bya:ℝ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)⊢ a ≤ b linarithAll goals completed! 🐙)
  have hbounded : Bornology.IsBounded (Set.Icc a b) := Icc_bounded _ _ha:ℝ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
  obtain ⟨ n, hn, ⟨ xmax, hmax, hconv⟩ ⟩ := (Heine_Borel (Set.Icc a b)).mp ⟨ hclosed, hbounded⟩ x hxh.intro.intro.intro.introa:ℝ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
  use xmax, hmaxrighta:ℝ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
  have hn_lower (j:ℕ) : n j ≥ j := why_7_6_3 hn jrighta:ℝ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
  have hconv' : Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax)) :=
    Filter.Tendsto.comp_of_continuous hmax (hf.continuousWithinAt hmax) (fun j ↦ hx (n j)) hconvrighta:ℝ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)) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
    apply lt_of_le_of_lt _ (hfx (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))j:ℕ⊢ m - 1 / (↑j + 1) ≤ m - 1 / (↑(n j) + 1)
    gcongrh.h.bc.ha:ℝ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
    exact hn_lower jAll goals completed! 🐙
  have hupper (j:ℕ) : f (x (n j)) ≤ m := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
    apply claim1hya:ℝ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
    simp only [Set.mem_image, E]hya:ℝ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 ∈ Set.Icc a b, f x_1 = f (x (n j))
    use x (n j), hx (n j)All goals completed! 🐙
  have hconvm : Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds m) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
    apply Filter.Tendsto.squeeze (g := fun j ↦ m - 1/(j+1:ℝ)) (h := fun j ↦ m) (f := fun j ↦ f (x (n j)))hga:ℝ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)hha:ℝ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) Filter.atTop (nhds m)hgfa:ℝ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))hfha:ℝ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 j => m
    .hga:ℝ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) convert Filter.Tendsto.const_sub m (c:=0) _h.e'_1.h.e'_3a:ℝ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 - 0hg.convert_4a:ℝ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 => 1 / (↑j + 1)) Filter.atTop (nhds 0)
      .h.e'_1.h.e'_3a:ℝ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 simpAll goals completed! 🐙
      exact tendsto_one_div_add_atTop_nhds_zero_natAll goals completed! 🐙
    .hha:ℝ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) Filter.atTop (nhds m) exact tendsto_const_nhdsAll goals completed! 🐙
    .hgfa:ℝ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)) intro jhgfa:ℝ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)) ≤ mj:ℕ⊢ (fun j => m - 1 / (↑j + 1)) j ≤ (fun j => f (x (n j))) j; exact le_of_lt (hlower j)All goals completed! 🐙
    exact hupperAll goals completed! 🐙
  exact tendsto_nhds_unique hconv' hconvmAll goals completed! 🐙

theorem declaration uses 'sorry'IsMinOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (Set.Icc a b)) :
  ∃ xmin ∈ Set.Icc a b, IsMinOn f (Set.Icc a b) xmin := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, IsMinOn f (Set.Icc a b) xmin
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : IsMaxOn (fun x ↦ x^2) (Set.Icc (-2) 2) 2 := by⊢ IsMaxOn (fun x => x ^ 2) (Set.Icc (-2) 2) 2 sorryAll goals completed! 🐙

declaration uses 'sorry'example : IsMaxOn (fun x ↦ x^2) (Set.Icc (-2) 2) (-2) := by⊢ IsMaxOn (fun x => x ^ 2) (Set.Icc (-2) 2) (-2) sorryAll goals completed! 🐙

theorem sSup.of_isMaxOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMaxOn f X x₀) :
  sSup (f '' X) = f x₀ := byf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ sSup (f '' X) = f x₀
  apply IsGreatest.csSup_eqHf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ IsGreatest (f '' X) (f x₀)
  simp [IsGreatest, mem_upperBounds]Hf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f a ≤ f x₀
  refine ⟨ ⟨x₀, hx₀, rfl ⟩, h ⟩All goals completed! 🐙

theorem sInf.of_isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMinOn f X x₀) :
  sInf (f '' X) = f x₀ := byf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ sInf (f '' X) = f x₀
  apply IsLeast.csInf_eqHf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ IsLeast (f '' X) (f x₀)
  simp [IsLeast, mem_lowerBounds]Hf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f x₀ ≤ f a
  refine ⟨ ⟨x₀, hx₀, rfl ⟩, h ⟩All goals completed! 🐙

theorem sSup.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax
  obtain ⟨ xmax, hmax, hhas ⟩ := IsMaxOn.of_continuous_on_compact h hfintro.introa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)xmax:ℝhmax:xmax ∈ Set.Icc a bhhas:IsMaxOn f (Set.Icc a b) xmax⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax
  exact ⟨ xmax, hmax, sSup.of_isMaxOn hmax hhas ⟩All goals completed! 🐙

theorem sInf.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (Set.Icc a b)) : ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin
  obtain ⟨ xmin, hmin, hhas ⟩ := IsMinOn.of_continuous_on_compact h hfintro.introa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)xmin:ℝhmin:xmin ∈ Set.Icc a bhhas:IsMinOn f (Set.Icc a b) xmin⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin
  exact ⟨ xmin, hmin, sInf.of_isMinOn hmin hhas ⟩All goals completed! 🐙

Вправа 9.6.1

declaration uses 'sorry'example : ∃ 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₀
  := by⊢ ∃ 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₀ sorryAll goals completed! 🐙

Вправа 9.6.1

declaration uses 'sorry'example : ∃ 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₀
  := by⊢ ∃ 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₀ sorryAll goals completed! 🐙

Вправа 9.6.1

declaration uses 'sorry'example : ∃ 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₀
  := by⊢ ∃ 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₀ sorryAll goals completed! 🐙

Вправа 9.6.1

declaration uses 'sorry'example : ∃ f: ℝ → ℝ, ¬ BddAboveOn f (Set.Icc (-1) 1) ∧ ¬ BddBelowOn f (Set.Icc (-1) 1) := by⊢ ∃ f, ¬BddAboveOn f (Set.Icc (-1) 1) ∧ ¬BddBelowOn f (Set.Icc (-1) 1) sorryAll goals completed! 🐙

end Chapter9