theorem helperForTheorem_1_4_subseq_tendsto (X : Type u) [MetricSpace X] {u : ℕ → CompletionViaFormalLimits X} {m : ℕ → ℕ} {x : ℕ → FormalLimit X} (hx : ∀ (n : ℕ), u (m n) = ⟦x n⟧) {k : ℕ → ℕ} (hkmono : Monotone k) (hA : ∀ (n j : ℕ), j ≥ k n → dist (↑(x n) j) (↑(x (n + 1)) j) < (1 / 2) ^ (n + 2)) (hB : ∀ (n j : ℕ), j ≥ k n → dist (↑(x (n + 1)) (k n)) (↑(x (n + 1)) j) < (1 / 2) ^ (n + 2)) (hy : CauchySeq fun (n : ℕ) => ↑(x n) (k n)) : Filter.Tendsto (fun (n : ℕ) => u (m n)) Filter.atTop (nhds ⟦⟨fun (n : ℕ) => ↑(x n) (k n), hy⟩⟧)

Helper for Theorem 1.4: the chosen subsequence converges to the diagonal class.

theorem completionViaFormalLimits_completeSpace (X : Type u) [MetricSpace X] : CompleteSpace (CompletionViaFormalLimits X)

Theorem 1.4: Let (X,d) be a metric space. Define Xbar as the set of equivalence classes of Cauchy sequences in X under (x_n) ~ (y_n) iff d(x_n,y_n) -> 0 as n -> infinity. For classes [(x_n)], [(y_n)] define d_{Xbar}([(x_n)],[(y_n)]) := lim_{n -> infinity} d(x_n,y_n), which is well-defined. Then (Xbar, d_{Xbar}) is complete.

theorem cauchySeq_const' {X : Type u} [MetricSpace X] (x : X) : CauchySeq fun (x_1 : ℕ) => x

The constant sequence in a metric space is Cauchy.

def completionViaFormalLimitsIota (X : Type u) [MetricSpace X] : X → CompletionViaFormalLimits X

The canonical map X → formal-limit completion, sending x to the constant sequence.

Equations

• completionViaFormalLimitsIota X x = ⟦⟨fun (x_1 : ℕ) => x, ⋯⟩⟧

theorem completionViaFormalLimitsIota_props (X : Type u) [MetricSpace X] : (∀ (x y : X), x = y ↔ completionViaFormalLimitsIota X x = completionViaFormalLimitsIota X y) ∧ (∀ (x y : X), dist x y = completionViaFormalLimitsDist X (completionViaFormalLimitsIota X x) (completionViaFormalLimitsIota X y)) ∧ Isometry (completionViaFormalLimitsIota X)

Proposition 1.25: Let (X,d) be a metric space, let X̄ be the set of equivalence classes of Cauchy sequences in X, and define d_{X̄}(LIM x_n, LIM y_n) := lim_{n→∞} d(x_n,y_n). Define iota : X → X̄ by sending x to the equivalence class of the constant sequence. (i) For all x, y ∈ X, one has x = y iff iota x = iota y. (ii) For all x, y ∈ X, one has d(x,y) = d_{X̄}(iota x, iota y). In particular, iota is an isometric embedding.

theorem completionViaFormalLimitsIota_eq_iff {X : Type u} [MetricSpace X] (x y : X) : x = y ↔ completionViaFormalLimitsIota X x = completionViaFormalLimitsIota X y

Equality in X is equivalent to equality in the formal completion via iota.

theorem completionViaFormalLimitsIota_dist {X : Type u} [MetricSpace X] (x y : X) : dist x y = completionViaFormalLimitsDist X (completionViaFormalLimitsIota X x) (completionViaFormalLimitsIota X y)

The canonical map into the formal completion preserves distances.

theorem completionViaFormalLimitsIota_isometry {X : Type u} [MetricSpace X] : Isometry (completionViaFormalLimitsIota X)

The canonical embedding into the formal completion is an isometry.

theorem helperForProposition_1_26_mk_mem_closure_range_iota {X : Type u} [MetricSpace X] (x : FormalLimit X) : ⟦x⟧ ∈ closure (Set.range (completionViaFormalLimitsIota X))

Helper for Proposition 1.26: each formal limit class lies in the closure of the canonical image of X.

theorem helperForProposition_1_26_denseRange_iota (X : Type u) [MetricSpace X] : DenseRange (completionViaFormalLimitsIota X)

Helper for Proposition 1.26: the canonical map into the completion has dense range.

theorem completionViaFormalLimits_closure_range (X : Type u) [MetricSpace X] : closure (Set.range (completionViaFormalLimitsIota X)) = Set.univ

Proposition 1.26: Let (X,d) be a metric space. Let (Xbar, d_{Xbar}) be the completion of X constructed by formal limits, and identify X with its canonical image in Xbar. Then Xbar is the closure of X in Xbar, i.e. Xbar = closure_X^{Xbar}.

theorem helperForProposition_1_27_tendsto_dist_to_limit {X : Type u} [MetricSpace X] (x : ℕ → X) {x0 : X} (hlim : Filter.Tendsto x Filter.atTop (nhds x0)) : Filter.Tendsto (fun (n : ℕ) => dist (x n) x0) Filter.atTop (nhds 0)

Helper for Proposition 1.27: convergence implies distances to the limit tend to zero.

theorem helperForProposition_1_27_formalLimitRel_const_of_tendsto {X : Type u} [MetricSpace X] (x : ℕ → X) {x0 : X} (hx : CauchySeq x) (hlim : Filter.Tendsto x Filter.atTop (nhds x0)) : FormalLimitRel X ⟨x, hx⟩ ⟨fun (x : ℕ) => x0, ⋯⟩

Helper for Proposition 1.27: relate a convergent Cauchy sequence to the constant formal limit.

theorem completionViaFormalLimits_limit_eq_iota {X : Type u} [MetricSpace X] (x : ℕ → X) {x0 : X} (hx : CauchySeq x) (hlim : Filter.Tendsto x Filter.atTop (nhds x0)) : ⟦⟨x, hx⟩⟧ = completionViaFormalLimitsIota X x0

Proposition 1.27: Let (X,d) be a metric space. Let (Xbar, d_{Xbar}) be the completion of X constructed via formal limits of Cauchy sequences, and identify X with its canonical image in Xbar. Let (x_n) be a Cauchy sequence in X that converges to x in X. Then the limit of (x_n) in (Xbar, d_{Xbar}) equals the embedded point x in Xbar, i.e. lim_{n -> infinity} x_n = LIM_{n -> infinity} x_n. A convergent Cauchy sequence has formal-limit class equal to the embedded limit.

theorem completeSpace_subtype_isClosed {X : Type u_1} [MetricSpace X] {Y : Set X} : CompleteSpace ↑Y → IsClosed Y

Proposition 1.33 (Complete subspaces are closed): Let (X,d) be a metric space and let Y ⊆ X be a subspace. If the metric subspace (Y, d|_{Y×Y}) is complete, then Y is closed in X.

theorem completeSpace_subtype_of_isClosed {X : Type u_1} [MetricSpace X] {Y : Set X} : CompleteSpace X → IsClosed Y → CompleteSpace ↑Y

Proposition 1.34 (Closed subspaces of complete spaces are complete): Let (X,d) be a complete metric space and let Y ⊆ X be a closed subset. Then the metric subspace (Y, d|_{Y×Y}) is complete.

theorem exists_completion_metricSpace (X : Type u) [MetricSpace X] : ∃ (Xbar : Type u) (inst : MetricSpace Xbar), CompleteSpace Xbar ∧ ∃ (iota : X → Xbar), Isometry iota ∧ DenseRange iota

Proposition 1.37 (Existence of completion): Let (X,d) be a metric space. There exists a complete metric space (X̄, d̄) and an isometric embedding ι : X → X̄ such that ι(X) is dense in X̄.