Documentation

Analysis.Section_9_4

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

Definition 9.4.1. Here we use the Mathlib definition of continuity. The hypothesis x₀ ∈ X is not needed!

source
@[reducible, inline]
noncomputable abbrev Chapter9.f_9_4_6 (x : ℝ) :
ℝ

Example 9.4.6.

Equations
Instances For
    source
    theorem Chapter9.ContinuousWithinAt.tfae (X : Set ℝ) (f : ℝ → ℝ) (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₀| < ε, ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε].TFAE

    Proposition 9.4.7 / Exercise 9.4.1.

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

    Remark 9.4.8.

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

    Proposition 9.4.9

    source
    theorem Chapter9.ContinuousWithinAt.sub {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) :
    ContinuousWithinAt (f - g) X x₀
    source
    theorem Chapter9.ContinuousWithinAt.max {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) :
    ContinuousWithinAt (f ⊔ g) X x₀
    source
    theorem Chapter9.ContinuousWithinAt.min {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) :
    ContinuousWithinAt (f ⊓ g) X x₀
    source
    theorem Chapter9.ContinuousWithinAt.mul' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) :
    ContinuousWithinAt (f * g) X x₀
    source
    theorem Chapter9.ContinuousWithinAt.div' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (hM : g x₀ ≠ 0) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) :
    ContinuousWithinAt (f / g) X x₀
    source
    theorem Chapter9.Continuous.exp {a : ℝ} (ha : a > 0) :
    Continuous fun (x : ℝ) => a ^ x

    Proposition 9.4.10 / Exercise 9.4.3

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

    Proposition 9.4.11 / Exercise 9.4.4

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

    Proposition 9.4.12

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

    Proposition 9.4.13 / Exercise 9.4.5

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

    Exercise 9.4.6

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

    Exercise 9.4.7