Аналіз 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

@[reducible, inline]

abbrev Chapter9.BddAboveOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Визначення 9.6.1

Equations

• Chapter9.BddAboveOn f X = ∃ (M : ℝ), ∀ x ∈ X, f x ≤ M

@[reducible, inline]

abbrev Chapter9.BddBelowOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Equations

• Chapter9.BddBelowOn f X = ∃ (M : ℝ), ∀ x ∈ X, -M ≤ f x

@[reducible, inline]

abbrev Chapter9.BddOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Equations

• Chapter9.BddOn f X = ∃ (M : ℝ), ∀ x ∈ X, |f x| ≤ M

theorem Chapter9.BddOn.iff (f : ℝ → ℝ) (X : Set ℝ) : BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X

Ремарка 9.6.2

theorem Chapter9.BddOn.iff' (f : ℝ → ℝ) (X : Set ℝ) : BddOn f X ↔ Bornology.IsBounded (f '' X)

theorem Chapter9.why_7_6_3 {n : ℕ → ℕ} (hn : StrictMono n) (j : ℕ) : n j ≥ j

theorem Chapter9.BddOn.of_continuous_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : BddOn f (Set.Icc a b)

Лема 7.6.3

theorem Chapter9.BddAboveOn.isMaxOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (h : IsMaxOn f X x₀) : BddAboveOn f X

Ремарка 9.6.6

theorem Chapter9.BddBelowOn.isMinOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (h : IsMinOn f X x₀) : BddBelowOn f X

theorem Chapter9.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

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

theorem Chapter9.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

theorem Chapter9.sSup.of_isMaxOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ X) (h : IsMaxOn f X x₀) : sSup (f '' X) = f x₀

theorem Chapter9.sInf.of_isMinOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ X) (h : IsMinOn f X x₀) : sInf (f '' X) = f x₀

theorem Chapter9.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

theorem Chapter9.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