@[reducible, inline]

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

Definition 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

Remark 9.6.2

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

theorem Chapter9.BddOn.of_bounded {f : ℝ → ℝ} {X : Set ℝ} {M : ℝ} (h : ∀ x ∈ X, |f x| ≤ M) : BddOn 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)

Lemma 9.6.3

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

Remark 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

Proposition 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