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

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:

• Continuity of functions

theorem Chapter9.ContinuousWithinAt.iff (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : ContinuousWithinAt f X x₀ ↔ Convergesto X f (f x₀) x₀

Визначення 9.4.1. Here we use the Mathlib definition of continuity. The hypothesis x ∈ X is not needed!

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_4_6 (x : ℝ) : ℝ

Приклад 9.4.6 -

Equations

• Chapter9.f_9_4_6 x = if x ≥ 0 then 1 else 0

theorem Chapter9.ContinuousWithinAt.tfae (X : Set ℝ) (f : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) : [ContinuousWithinAt f X x₀, ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun (n : ℕ) => f (a n)) Filter.atTop (nhds (f x₀)), ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε].TFAE

Твердження 9.4.7 / Вправа 9.4.1. It is possible that the hypothesis x₀ ∈ X is unnecessary.

theorem Chapter9.Filter.Tendsto.comp_of_continuous {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : x₀ ∈ X) (h_cont : ContinuousWithinAt f X x₀) {a : ℕ → ℝ} (ha : ∀ (n : ℕ), a n ∈ X) (hconv : Filter.Tendsto a Filter.atTop (nhds x₀)) : Filter.Tendsto (fun (n : ℕ) => f (a n)) Filter.atTop (nhds (f x₀))

Ремарка 9.4.8 -

theorem Chapter9.ContinuousWithinAt.add {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f + g) X x₀

theorem Chapter9.ContinuousWithinAt.sub {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f - g) X x₀

theorem Chapter9.ContinuousWithinAt.max {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f ⊔ g) X x₀

theorem Chapter9.ContinuousWithinAt.min {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f ⊓ g) X x₀

theorem Chapter9.ContinuousWithinAt.mul' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f * g) X x₀

theorem Chapter9.ContinuousWithinAt.div' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hM : g x₀ ≠ 0) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f / g) X x₀

theorem Chapter9.Continuous.exp {a : ℝ} (ha : a > 0) : Continuous fun (x : ℝ) => a ^ x

Твердження 9.4.10 / Вправа 9.4.3

theorem Chapter9.Continuous.exp' (p : ℝ) : ContinuousOn (fun (x : ℝ) => x ^ p) (Set.Ioi 0)

Твердження 9.4.11 / Вправа 9.4.4

theorem Chapter9.Continuous.abs : Continuous fun (x : ℝ) => |x|

Твердження 9.4.12

theorem Chapter9.ContinuousWithinAt.comp {x : ℝ} {X Y : Set ℝ} {f g : ℝ → ℝ} (hf : ∀ x ∈ X, f x ∈ Y) {x₀ : ℝ} (hx₀ : x ∈ X) (hf_cont : ContinuousWithinAt f X x₀) (hg_cont : ContinuousWithinAt g Y (f x₀)) : ContinuousWithinAt (g ∘ f) X x₀

Твердження 9.4.13 / Вправа 9.4.5

theorem Chapter9.ContinuousOn.restrict {X Y : Set ℝ} {f : ℝ → ℝ} (hY : Y ⊆ X) (hf : ContinuousOn f X) : ContinuousOn f Y

Вправа 9.4.6

theorem Chapter9.Continuous.polynomial {n : ℕ} (c : Fin n → ℝ) : Continuous fun (x : ℝ) => ∑ i : Fin n, c i * x ^ ↑i

Вправа 9.4.7