theorem uniformLimit_continuousAt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (x0 : X) (hcont : ∀ (n : ℕ), ContinuousAt (fseq n) x0) : ContinuousAt f x0

Theorem 3.3.1: [Uniform limits preserve continuity I] Suppose (X, d_X) and (Y, d_Y) are metric spaces, f^{(n)} : X → Y converges uniformly to f : X → Y, and x0 ∈ X. If each f^{(n)} is continuous at x0, then f is continuous at x0.

theorem uniformLimit_continuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (hcont : ∀ (n : ℕ), Continuous (fseq n)) : Continuous f

Theorem 3.3.2: [Uniform limits preserve continuity] Suppose (X, d_X) and (Y, d_Y) are metric spaces and f^{(n)} : X → Y converges uniformly to f : X → Y. If each f^{(n)} is continuous at every point of X, then f is continuous at every point of X.

theorem helperForProp_3_3_3_comap_neBot {X : Type u_1} [TopologicalSpace X] {E : Set X} {x0 : X} (hx0 : x0 ∈ closure E) : (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)).NeBot

Helper for Proposition 3.3.3: the comap filter at an adherent point is nontrivial.

theorem helperForProp_3_3_3_eventually_dist_lt_of_hlim {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {F : Filter X} {g : X → Y} {l : Y} (hlim : Filter.Tendsto g F (nhds l)) (ε : ℝ) : ε > 0 → {x : X | dist (g x) l < ε} ∈ F

Helper for Proposition 3.3.3: convert a limit into an eventual distance bound.

theorem helperForProp_3_3_3_cauchySeq_ell {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {E : Set X} {fseq : ℕ → ↑E → Y} {f : ↑E → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (x0 : X) (hx0 : x0 ∈ closure E) (ℓ : ℕ → Y) (hlim : ∀ (n : ℕ), Filter.Tendsto (fseq n) (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)) (nhds (ℓ n))) : CauchySeq ℓ

Helper for Proposition 3.3.3: the sequence of limits ℓ is Cauchy.

theorem helperForProp_3_3_3_tendsto_f_limit {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {E : Set X} {fseq : ℕ → ↑E → Y} {f : ↑E → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (x0 : X) (ℓ : ℕ → Y) (hlim : ∀ (n : ℕ), Filter.Tendsto (fseq n) (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)) (nhds (ℓ n))) {l : Y} (hl : Filter.Tendsto ℓ Filter.atTop (nhds l)) : Filter.Tendsto f (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)) (nhds l)

Helper for Proposition 3.3.3: the uniform limit has the expected limit at x0.

theorem uniformLimit_interchange_limits {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] [CompleteSpace Y] {E : Set X} {fseq : ℕ → ↑E → Y} {f : ↑E → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (x0 : X) (hx0 : x0 ∈ closure E) (ℓ : ℕ → Y) (hlim : ∀ (n : ℕ), Filter.Tendsto (fseq n) (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)) (nhds (ℓ n))) : ∃ (l : Y), Filter.Tendsto ℓ Filter.atTop (nhds l) ∧ Filter.Tendsto f (Filter.comap (fun (x : ↑E) => ↑x) (nhds x0)) (nhds l)

Proposition 3.3.3: [Interchange of limits and uniform limits] Let (X, d_X) and (Y, d_Y) be metric spaces with Y complete, let E ⊆ X, and let f^{(n)} : E → Y converge uniformly on E to f : E → Y. If x0 is an adherent point of E and each f^{(n)} has a limit at x0 along E equal to ℓ n, then ℓ n converges and f has a limit at x0 along E, with the two iterated limits equal.

theorem helperForProp_3_3_4_unif_dist_lt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (x : X), dist (fseq n x) (f x) < ε

Helper for Proposition 3.3.4: uniform convergence with the distance order reversed.

theorem helperForProp_3_3_4_dist_triangle5 {Y : Type u_1} [MetricSpace Y] (a b c d e : Y) : dist a e ≤ dist a b + dist b c + dist c d + dist d e

Helper for Proposition 3.3.4: a 5-point triangle inequality chain.

theorem uniformLimit_eval_tendsto {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (hcont : ∀ (n : ℕ), Continuous (fseq n)) {xseq : ℕ → X} {x : X} (hx : Filter.Tendsto xseq Filter.atTop (nhds x)) : Filter.Tendsto (fun (n : ℕ) => fseq n (xseq n)) Filter.atTop (nhds (f x))

Proposition 3.3.4: Let (X, d_X) and (Y, d_Y) be metric spaces. Let f^{(n)} : X → Y be continuous for each n, and suppose f^{(n)} → f : X → Y uniformly on X. If (x^{(n)}) is a sequence in X with x^{(n)} → x, then f^{(n)}(x^{(n)}) → f(x) in Y.

def IsBoundedFunction {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : Prop

Definition 3.4: A function f : X → Y between metric spaces is bounded if its image lies in some ball, i.e., there exist y0 ∈ Y and R > 0 such that dist (f x) y0 < R for all x ∈ X.

Equations

• IsBoundedFunction f = ∃ (y0 : Y) (R : ℝ), 0 < R ∧ ∀ (x : X), dist (f x) y0 < R

theorem helperForProp_3_3_5_isBounded_of_uniform_dist_lt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {f g : X → Y} {ε : ℝ} (hε : 0 < ε) (hbounded : IsBoundedFunction g) (hfg : ∀ (x : X), dist (f x) (g x) < ε) : IsBoundedFunction f

Helper for Proposition 3.3.5: boundedness is stable under a uniform perturbation.

theorem uniformLimit_bounded {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (hbounded : ∀ (n : ℕ), IsBoundedFunction (fseq n)) : IsBoundedFunction f

Proposition 3.3.5: [Uniform limits preserve boundedness] Let (X, d_X) and (Y, d_Y) be metric spaces. Let f^{(n)} : X → Y converge uniformly to f : X → Y. If each f^{(n)} is bounded on X, then f is bounded on X.

theorem uniformLimit_boundedness {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {fseq : ℕ → X → Y} {f : X → Y} (h_unif : TendstoUniformly fseq f Filter.atTop) (hbounded : ∀ (n : ℕ), IsBoundedFunction (fseq n)) : IsBoundedFunction f

Proposition 3.3.6: [Uniform limits preserve boundedness] Let (X, d_X) and (Y, d_Y) be metric spaces. Let f^{(n)} : X → Y converge uniformly to f : X → Y. If each f^{(n)} is bounded on X, then f is bounded on X.