def IsSubsequenceFrom {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (y : ℕ → X) : Prop

Definition 1.16 (Subsequences): Let (X,d) be a metric space, let (x^(n))_{n=m}^infty be a sequence in X, and let (n_j) be a strictly increasing sequence of integers with n_j >= m (equivalently, m <= n_1 < n_2 < n_3 < ...). The sequence (x^(n_j))_{j=1}^infty is called a subsequence of (x^(n))_{n=m}^infty.

Equations

• IsSubsequenceFrom x m y = ∃ (n : ℕ → ℕ), StrictMono n ∧ (∀ (j : ℕ), m ≤ n j) ∧ y = fun (j : ℕ) => x (n j)

theorem tendsto_subseq_of_tendsto {X : Type u_1} [MetricSpace X] (x : ℕ → X) {x0 : X} (hx : Filter.Tendsto x Filter.atTop (nhds x0)) {n : ℕ → ℕ} (hn : StrictMono n) : Filter.Tendsto (fun (j : ℕ) => x (n j)) Filter.atTop (nhds x0)

Lemma 1.2: Let (X,d) be a metric space, (x^{(n)}) a sequence in X, and x0 ∈ X. If x^{(n)} → x0 as n → ∞, then for every strictly increasing sequence of indices (n_j), the subsequence (x^{(n_j)}) converges to x0.

def IsLimitPointSeqFrom {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) : Prop

Definition 1.17 (Limit point of a sequence): Let (X,d) be a metric space, let m be a starting index, and let (x^(n))_{n=m}^infty be a sequence in X. A point L ∈ X is called a limit point of (x^(n))_{n=m}^infty if for every N ≥ m and every ε > 0 there exists an integer n ≥ N such that d(x^(n), L) ≤ ε.

Equations

• IsLimitPointSeqFrom x m L = ∀ N ≥ m, ∀ ε > 0, ∃ n ≥ N, dist (x n) L ≤ ε

theorem isLimitPointSeqFrom_iff {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) : IsLimitPointSeqFrom x m L ↔ ∀ N ≥ m, ∀ ε > 0, ∃ n ≥ N, dist (x n) L ≤ ε

A point is a limit point of a sequence from index m if every tail gets within any ε > 0.

def IsCauchySeqFrom {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) : Prop

Definition 1.18 (Cauchy sequence): Let (X,d) be a metric space, let m ∈ ℕ, and let (x^(n))_{n=m}^∞ be a sequence in X. The sequence is called a Cauchy sequence if for every ε > 0 there exists an integer N ≥ m such that d(x^(j), x^(k)) < ε for all j, k ≥ N.

Equations

• IsCauchySeqFrom x m = ∀ ε > 0, ∃ N ≥ m, ∀ j ≥ N, ∀ k ≥ N, dist (x j) (x k) < ε

theorem isCauchySeqFrom_imp_cauchySeq_tail {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) : IsCauchySeqFrom x m → CauchySeq fun (n : ℕ) => x (n + m)

A Cauchy sequence from index m gives a CauchySeq for the shifted tail.

theorem cauchySeq_tail_imp_isCauchySeqFrom {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) : (CauchySeq fun (n : ℕ) => x (n + m)) → IsCauchySeqFrom x m

A CauchySeq of the shifted tail yields a Cauchy sequence from index m.

theorem isCauchySeqFrom_iff_cauchySeq_tail {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) : IsCauchySeqFrom x m ↔ CauchySeq fun (n : ℕ) => x (n + m)

A sequence is Cauchy from index m iff its shifted tail is a CauchySeq.

theorem helperForProposition_1_19_one_div_pos (k : ℕ) : 0 < 1 / (↑k + 1)

Helper for Proposition 1.19: the bound 1/(k+1) is always positive.

theorem helperForProposition_1_19_extend_tail {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) (h : ∀ ε > 0, ∀ N ≥ m, ∃ n ≥ N, dist (x n) L < ε) (ε : ℝ) : ε > 0 → ∀ (N : ℕ), ∃ n ≥ N, dist (x n) L < ε

Helper for Proposition 1.19: extend the tail condition to any starting index.

theorem helperForProposition_1_19_tendsto_of_one_div_bound (f : ℕ → ℝ) (hf0 : ∀ (k : ℕ), 0 ≤ f k) (hf : ∀ (k : ℕ), f k ≤ 1 / (↑k + 1)) : Filter.Tendsto f Filter.atTop (nhds 0)

Helper for Proposition 1.19: a squeeze argument for the bound 1/(k+1).

theorem limitPointSeqFrom_iff_subseq_tendsto {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) : (∀ ε > 0, ∀ N ≥ m, ∃ n ≥ N, dist (x n) L < ε) ↔ ∃ (n : ℕ → ℕ), StrictMono n ∧ m ≤ n 0 ∧ Filter.Tendsto (fun (j : ℕ) => dist (x (n j)) L) Filter.atTop (nhds 0)

Proposition 1.19: Let (X,d) be a metric space, let (x^(n))_{n=m}^infty be a sequence in X, and let L ∈ X. The following statements are equivalent: (i) for every ε > 0 and every N ≥ m, there exists n ≥ N such that d(x^(n), L) < ε; (ii) there exists a strictly increasing sequence of integers (n_j)_{j=1}^∞ with n_1 ≥ m such that d(x^(n_j), L) → 0 as j → ∞.

theorem helperForLemma_1_3_dist_lt_of_tail_dist_lt {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (x0 : X) {N0 j : ℕ} {r : ℝ} (h : ∀ n ≥ N0, dist (x (n + m)) x0 < r) (hj : N0 + m ≤ j) : dist (x j) x0 < r

Helper for Lemma 1.3: extend a tail distance bound to any index beyond N0 + m.

theorem convergentSeqFrom_isCauchy {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) {x0 : X} (hx : Filter.Tendsto (fun (n : ℕ) => x (n + m)) Filter.atTop (nhds x0)) : IsCauchySeqFrom x m

Lemma 1.3 (Convergent sequences are Cauchy): Let (X,d) be a metric space and let (x^(n))_{n=m}^∞ be a sequence in X such that x^(n) → x0 ∈ X as n → ∞. Then (x^(n))_{n=m}^∞ is a Cauchy sequence, i.e., for every ε > 0 there exists N ≥ m such that for all n, n' ≥ N one has d(x^(n), x^(n')) < ε. A convergent tail of a sequence is Cauchy from its starting index.

theorem helperForLemma_1_4_eventually_ge_subseqIndex {n : ℕ → ℕ} (hn : StrictMono n) (N : ℕ) : ∃ (J : ℕ), ∀ j ≥ J, N ≤ n j

Helper for Lemma 1.4: a strictly increasing subsequence is eventually beyond any index.

theorem helperForLemma_1_4_choose_subseqIndex_close {X : Type u_1} [MetricSpace X] (x : ℕ → X) {x0 : X} {n : ℕ → ℕ} (hn : StrictMono n) (hsub : Filter.Tendsto (fun (j : ℕ) => x (n j)) Filter.atTop (nhds x0)) {N : ℕ} {ε : ℝ} (hε : 0 < ε) : ∃ (j : ℕ), N ≤ n j ∧ dist (x (n j)) x0 < ε

Helper for Lemma 1.4: pick a subsequence index beyond N that is ε-close to x0.

theorem tendsto_of_cauchySeqFrom_of_subseq_tendsto {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) {x0 : X} (hx : IsCauchySeqFrom x m) {n : ℕ → ℕ} (hn : StrictMono n) (hnm : ∀ (j : ℕ), m ≤ n j) (hsub : Filter.Tendsto (fun (j : ℕ) => x (n j)) Filter.atTop (nhds x0)) : Filter.Tendsto (fun (k : ℕ) => x (k + m)) Filter.atTop (nhds x0)

Lemma 1.4: Let (X,d) be a metric space and let (x^{(n)})_{n=m}^∞ be a Cauchy sequence in X. Suppose there exists a subsequence (x^{(n_j)}) and a point x0 ∈ X such that x^{(n_j)} → x0 as j → ∞. Then x^{(n)} → x0 as n → ∞.

theorem helperForLemma_1_5_le_apply_of_le {n : ℕ → ℕ} (hn : StrictMono n) {N j : ℕ} (hNj : N ≤ j) : N ≤ n j

Helper for Lemma 1.5: a strictly increasing index map dominates any lower bound.

theorem cauchySeqFrom_subseq {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (y : ℕ → X) (hx : IsCauchySeqFrom x m) (hsub : IsSubsequenceFrom x m y) : IsCauchySeqFrom y 0

Lemma 1.5 (Subsequence of Cauchy sequence is Cauchy): Let (X,d) be a metric space and let (x^(n))_{n=m}^∞ be a Cauchy sequence in X. Then every subsequence (x^(n_j))_{j=1}^∞ of (x^(n))_{n=m}^∞ is also a Cauchy sequence.

def IsCompleteMetricSpace (X : Type u_1) [MetricSpace X] : Prop

Definition 1.19 (Complete metric space): A metric space (X,d) is complete if every Cauchy sequence converges to a point of X, i.e., for every Cauchy sequence there exists x ∈ X such that d(x_n, x) → 0 as n → ∞.

Equations

• IsCompleteMetricSpace X = ∀ (x : ℕ → X), CauchySeq x → ∃ (L : X), Filter.Tendsto x Filter.atTop (nhds L)

theorem isCompleteMetricSpace_iff_completeSpace (X : Type u_1) [MetricSpace X] : IsCompleteMetricSpace X ↔ CompleteSpace X

The book's Cauchy-sequence definition of completeness is equivalent to CompleteSpace.

theorem completeSpace_subtype_closed {X : Type u_1} [MetricSpace X] {Y : Set X} : (CompleteSpace ↑Y → IsClosed Y) ∧ (CompleteSpace X → IsClosed Y → CompleteSpace ↑Y)

Proposition 1.20: Let (X,d) be a metric space and let Y ⊆ X be equipped with the subspace metric d|_{Y×Y}. (a) If (Y, d|_{Y×Y}) is complete, then Y is closed in X. (b) If (X,d) is complete and Y is closed in X, then (Y, d|_{Y×Y}) is complete.

theorem helperForProposition_1_21_exists_index_ge_m {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) (hL : ∀ ε > 0, ∀ N ≥ m, ∃ n ≥ N, dist (x n) L < ε) (ε : ℝ) : ε > 0 → ∃ n ≥ m, dist (x n) L < ε

Helper for Proposition 1.21: specialize the limit-point hypothesis at N = m.

theorem helperForProposition_1_21_mem_tail_set {X : Type u_1} (x : ℕ → X) (m n : ℕ) (hn : n ≥ m) : x n ∈ {a : X | ∃ n ≥ m, a = x n}

Helper for Proposition 1.21: an index n ≥ m gives membership in the tail set.

theorem limitPointSeqFrom_adherent_point {X : Type u_1} [MetricSpace X] (x : ℕ → X) (m : ℕ) (L : X) (hL : ∀ ε > 0, ∀ N ≥ m, ∃ n ≥ N, dist (x n) L < ε) (ε : ℝ) : ε > 0 → ∃ a ∈ {a : X | ∃ n ≥ m, a = x n}, dist a L < ε

Proposition 1.21: Let (X,d) be a metric space, let m ∈ ℕ, and let (x^(n))_{n=m}^∞ be a sequence in X. Let L ∈ X. Assume that L is a limit point of the sequence, i.e., for every ε > 0 and every N ≥ m there exists n ≥ N such that d(x^(n), L) < ε. Then L is an adherent point of the set A := {x^(n) : n ≥ m}, i.e., for every ε > 0 there exists a ∈ A such that d(a, L) < ε. A limit point of a tail of a sequence is an adherent point of the tail set.

theorem cauchySeq_limit_unique {X : Type u_1} [MetricSpace X] (x : ℕ → X) {x0 y0 : X} (hx : CauchySeq x) (hx' : Filter.Tendsto x Filter.atTop (nhds x0)) (hy' : Filter.Tendsto x Filter.atTop (nhds y0)) : x0 = y0

Proposition 1.22: Let (X,d) be a metric space, and let (x_n)_{n∈ℕ} be a Cauchy sequence in X. If x_n → x and x_n → y for some x,y ∈ X, then x = y. Equivalently, a Cauchy sequence in a metric space has at most one limit.

theorem cauchySeq_limit_unique' {X : Type u_1} [MetricSpace X] (x : ℕ → X) {x0 y0 : X} (hx : CauchySeq x) (hx' : Filter.Tendsto x Filter.atTop (nhds x0)) (hy' : Filter.Tendsto x Filter.atTop (nhds y0)) : x0 = y0

A Cauchy sequence in a metric space has at most one limit.

def FormalLimit (X : Type u) [MetricSpace X] : Type u

Definition 1.20 (Completion via formal limits): Let (X,d) be a metric space. (1) For every Cauchy sequence (x_n)_{n=1}^∞ in X, introduce a formal symbol LIM_{n→∞} x_n. (2) Define an equivalence relation ~ on such formal symbols by LIM x_n ~ LIM y_n iff lim_{n→∞} d(x_n,y_n) = 0. (3) Define X̄ to be the set of equivalence classes modulo ~. (4) Define d_{X̄} : X̄ × X̄ → [0,∞) by d_{X̄}(LIM x_n, LIM y_n) := lim_{n→∞} d(x_n,y_n), where representatives are chosen from the corresponding equivalence classes.

Equations

• FormalLimit X = { x : ℕ → X // CauchySeq x }

def FormalLimitRel (X : Type u) [MetricSpace X] (x y : FormalLimit X) : Prop

The relation identifying two formal limits when their pointwise distance tends to 0.

Equations

• FormalLimitRel X x y = Filter.Tendsto (fun (n : ℕ) => dist (↑x n) (↑y n)) Filter.atTop (nhds 0)

theorem helperForProposition_1_23_refl (X : Type u) [MetricSpace X] (x : FormalLimit X) : FormalLimitRel X x x

Helper for Proposition 1.23: reflexivity of the formal-limit relation.

theorem helperForProposition_1_23_symm (X : Type u) [MetricSpace X] (x y : FormalLimit X) : FormalLimitRel X x y → FormalLimitRel X y x

Helper for Proposition 1.23: symmetry of the formal-limit relation.

theorem helperForProposition_1_23_trans (X : Type u) [MetricSpace X] (x y z : FormalLimit X) : FormalLimitRel X x y → FormalLimitRel X y z → FormalLimitRel X x z

Helper for Proposition 1.23: transitivity of the formal-limit relation.

theorem formalLimitRel_equivalence (X : Type u) [MetricSpace X] : Equivalence (FormalLimitRel X)

Proposition 1.23: Let (X,d) be a metric space, and let C be the set of all Cauchy sequences in X. For Cauchy sequences (x_n) and (y_n) define a relation ~ on the set of formal limits {LIM_{n→∞} x_n : (x_n) ∈ C} by LIM x_n ~ LIM y_n iff lim_{n→∞} d(x_n,y_n) = 0. Then ~ is an equivalence relation.

def FormalLimitSetoid (X : Type u) [MetricSpace X] : Setoid (FormalLimit X)

Helper for Proposition 1.24: the setoid induced by the formal-limit relation.

Equations

• FormalLimitSetoid X = { r := FormalLimitRel X, iseqv := ⋯ }

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

Helper for Proposition 1.24: the completion via formal limits as a quotient of formal symbols.

Equations

• CompletionViaFormalLimits X = Quotient (FormalLimitSetoid X)

theorem helperForProposition_1_24_distSeq_cauchy (X : Type u) [MetricSpace X] (x y : FormalLimit X) : CauchySeq fun (n : ℕ) => dist (↑x n) (↑y n)

Helper for Proposition 1.24: the pointwise distance between two Cauchy representatives is itself a Cauchy sequence.

noncomputable def helperForProposition_1_24_formalLimitDist (X : Type u) [MetricSpace X] (x y : FormalLimit X) : ℝ

Helper for Proposition 1.24: define the representative-level distance via limUnder.

Equations

• helperForProposition_1_24_formalLimitDist X x y = limUnder Filter.atTop fun (n : ℕ) => dist (↑x n) (↑y n)

theorem helperForProposition_1_24_formalLimitDist_tendsto (X : Type u) [MetricSpace X] (x y : FormalLimit X) : Filter.Tendsto (fun (n : ℕ) => dist (↑x n) (↑y n)) Filter.atTop (nhds (helperForProposition_1_24_formalLimitDist X x y))

Helper for Proposition 1.24: the representative-level distance is the limit of pointwise distances.

theorem helperForProposition_1_24_formalLimitDist_congr (X : Type u) [MetricSpace X] (x y x' y' : FormalLimit X) : FormalLimitRel X x x' → FormalLimitRel X y y' → helperForProposition_1_24_formalLimitDist X x y = helperForProposition_1_24_formalLimitDist X x' y'

Helper for Proposition 1.24: the representative-level distance respects the formal-limit equivalence relation.

noncomputable def completionViaFormalLimitsDist (X : Type u) [MetricSpace X] : CompletionViaFormalLimits X → CompletionViaFormalLimits X → ℝ

Helper for Proposition 1.24: the distance on the formal completion, defined by limits of distances.

Equations

• completionViaFormalLimitsDist X qx qy = Quotient.liftOn₂ qx qy (fun (x y : FormalLimit X) => helperForProposition_1_24_formalLimitDist X x y) ⋯

theorem helperForProposition_1_24_formalLimit_coe_cauchy (X : Type u) [MetricSpace X] (x : FormalLimit X) : CauchySeq fun (n : ℕ) => ↑(↑x n)

Helper for Proposition 1.24: the coerced sequence of a formal limit is Cauchy in the completion.

noncomputable def helperForProposition_1_24_formalLimit_to_uniformCompletion (X : Type u) [MetricSpace X] (x : FormalLimit X) : UniformSpace.Completion X

Helper for Proposition 1.24: send a formal limit to the limit of its coerced sequence.

Equations

• helperForProposition_1_24_formalLimit_to_uniformCompletion X x = limUnder Filter.atTop fun (n : ℕ) => ↑(↑x n)

theorem helperForProposition_1_24_formalLimit_to_uniformCompletion_tendsto (X : Type u) [MetricSpace X] (x : FormalLimit X) : Filter.Tendsto (fun (n : ℕ) => ↑(↑x n)) Filter.atTop (nhds (helperForProposition_1_24_formalLimit_to_uniformCompletion X x))

Helper for Proposition 1.24: the coerced sequence converges to its chosen completion point.

theorem helperForProposition_1_24_formalLimit_to_uniformCompletion_congr (X : Type u) [MetricSpace X] (x y : FormalLimit X) : FormalLimitRel X x y → helperForProposition_1_24_formalLimit_to_uniformCompletion X x = helperForProposition_1_24_formalLimit_to_uniformCompletion X y

Helper for Proposition 1.24: equivalent formal limits map to the same completion point.

noncomputable def helperForProposition_1_24_completion_to_uniformCompletion (X : Type u) [MetricSpace X] : CompletionViaFormalLimits X → UniformSpace.Completion X

Helper for Proposition 1.24: the map from the formal completion to the uniform completion.

Equations

• helperForProposition_1_24_completion_to_uniformCompletion X = Quotient.lift (helperForProposition_1_24_formalLimit_to_uniformCompletion X) ⋯

theorem helperForProposition_1_24_tendsto_pow_one_half : Filter.Tendsto (fun (n : ℕ) => (1 / 2) ^ n) Filter.atTop (nhds 0)

Helper for Proposition 1.24: powers of 1/2 tend to 0.

theorem helperForProposition_1_24_pow_eventually_lt (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, (1 / 2) ^ n < ε

Helper for Proposition 1.24: powers of 1/2 are eventually below any positive threshold.

theorem helperForProposition_1_24_completion_to_uniformCompletion_surjective (X : Type u) [MetricSpace X] : Function.Surjective (helperForProposition_1_24_completion_to_uniformCompletion X)

Helper for Proposition 1.24: the map to the uniform completion is surjective.

theorem helperForProposition_1_24_completion_to_uniformCompletion_injective (X : Type u) [MetricSpace X] : Function.Injective (helperForProposition_1_24_completion_to_uniformCompletion X)

Helper for Proposition 1.24: the map to the uniform completion is injective.

theorem completionViaFormalLimits_equiv_uniformCompletion (X : Type u) [MetricSpace X] : Nonempty (CompletionViaFormalLimits X ≃ UniformSpace.Completion X)

Helper for Proposition 1.24: the formal-limit completion is (noncanonically) equivalent to the uniform completion.

theorem helperForProposition_1_24_completionDist_self (X : Type u) [MetricSpace X] (q : CompletionViaFormalLimits X) : completionViaFormalLimitsDist X q q = 0

Helper for Proposition 1.24: dist vanishes on identical classes.

theorem helperForProposition_1_24_completionDist_comm (X : Type u) [MetricSpace X] (qx qy : CompletionViaFormalLimits X) : completionViaFormalLimitsDist X qx qy = completionViaFormalLimitsDist X qy qx

Helper for Proposition 1.24: the formal-limit distance is symmetric.

theorem helperForProposition_1_24_completionDist_triangle (X : Type u) [MetricSpace X] (qx qy qz : CompletionViaFormalLimits X) : completionViaFormalLimitsDist X qx qz ≤ completionViaFormalLimitsDist X qx qy + completionViaFormalLimitsDist X qy qz

Helper for Proposition 1.24: the formal-limit distance satisfies the triangle inequality.

theorem helperForProposition_1_24_completionDist_eq_zero (X : Type u) [MetricSpace X] {qx qy : CompletionViaFormalLimits X} : completionViaFormalLimitsDist X qx qy = 0 → qx = qy

Helper for Proposition 1.24: distance zero gives equality in the quotient.

theorem helperForProposition_1_24_completion_edist_dist (X : Type u) [MetricSpace X] (x y : CompletionViaFormalLimits X) : (fun (a b : CompletionViaFormalLimits X) => ENNReal.ofReal (completionViaFormalLimitsDist X a b)) x y = ENNReal.ofReal (completionViaFormalLimitsDist X x y)

Helper for Proposition 1.24: the edist field is ENNReal.ofReal of the distance.

noncomputable def helperForProposition_1_24_completionPseudoMetricSpace (X : Type u) [MetricSpace X] : PseudoMetricSpace (CompletionViaFormalLimits X)

Helper for Proposition 1.24: the pseudo-metric structure on the formal completion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def helperForProposition_1_24_completionMetricSpace (X : Type u) [MetricSpace X] : MetricSpace (CompletionViaFormalLimits X)

Helper for Proposition 1.24: the formal-limit completion carries a metric-space structure.

Equations

• helperForProposition_1_24_completionMetricSpace X = { toPseudoMetricSpace := helperForProposition_1_24_completionPseudoMetricSpace X, eq_of_dist_eq_zero := ⋯ }

theorem completionViaFormalLimitsDist_wellDefined_and_metricSpace (X : Type u) [MetricSpace X] : (∀ (x y x' y' : FormalLimit X), FormalLimitRel X x x' → FormalLimitRel X y y' → completionViaFormalLimitsDist X ⟦x⟧ ⟦y⟧ = completionViaFormalLimitsDist X ⟦x'⟧ ⟦y'⟧) ∧ Nonempty (MetricSpace (CompletionViaFormalLimits X))

Proposition 1.24: Let (X,d) be a metric space. Define X̄ as the set of equivalence classes of Cauchy sequences in X, where two Cauchy sequences (x_n) and (y_n) are equivalent if d(x_n,y_n) → 0 as n → ∞. For classes [(x_n)], [(y_n)] ∈ X̄, define d_{X̄}([(x_n)],[(y_n)]) := lim_{n→∞} d(x_n,y_n). Then d_{X̄} is well-defined and (X̄, d_{X̄}) is a metric space.

theorem completionViaFormalLimitsDist_wellDefined (X : Type u) [MetricSpace X] (x y x' y' : FormalLimit X) : FormalLimitRel X x x' → FormalLimitRel X y y' → completionViaFormalLimitsDist X ⟦x⟧ ⟦y⟧ = completionViaFormalLimitsDist X ⟦x'⟧ ⟦y'⟧

Helper for Proposition 1.24: the formal-limit distance does not depend on the chosen Cauchy representatives.

noncomputable instance completionViaFormalLimitsMetricSpace (X : Type u) [MetricSpace X] : MetricSpace (CompletionViaFormalLimits X)

Helper for Proposition 1.24: the formal-limit completion carries a metric-space structure via the formal-limit distance.

Equations

• completionViaFormalLimitsMetricSpace X = helperForProposition_1_24_completionMetricSpace X

theorem helperForTheorem_1_4_chooseRepresentatives (X : Type u) [MetricSpace X] (u : ℕ → CompletionViaFormalLimits X) : ∃ (x : ℕ → FormalLimit X), ∀ (n : ℕ), u n = ⟦x n⟧

Helper for Theorem 1.4: choose representatives for a sequence in the quotient.

theorem helperForTheorem_1_4_reindex_cauchy (X : Type u) [MetricSpace X] (z : FormalLimit X) {m : ℕ → ℕ} (hm : StrictMono m) : CauchySeq fun (n : ℕ) => ↑z (m n)

Helper for Theorem 1.4: reindexing a Cauchy representative stays Cauchy.

theorem helperForTheorem_1_4_equiv_reindex (X : Type u) [MetricSpace X] (z : FormalLimit X) {m : ℕ → ℕ} (hm : StrictMono m) : FormalLimitRel X z ⟨fun (n : ℕ) => ↑z (m n), ⋯⟩

Helper for Theorem 1.4: a formal limit is equivalent to any strictly monotone reindexing.

theorem helperForTheorem_1_4_eventually_dist_lt (X : Type u) [MetricSpace X] {x y : FormalLimit X} {r : ℝ} (h : helperForProposition_1_24_formalLimitDist X x y < r) : ∃ (N : ℕ), ∀ n ≥ N, dist (↑x n) (↑y n) < r

Helper for Theorem 1.4: if the formal-limit distance is below r, then pointwise distances are eventually below r.

theorem helperForTheorem_1_4_pow_eventually_lt (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, (1 / 2) ^ (n + 2) < ε

Helper for Theorem 1.4: powers of 1/2 are eventually below any positive threshold.

theorem helperForTheorem_1_4_cauchySeq_subseq_geometric (X : Type u) [MetricSpace X] (u : ℕ → CompletionViaFormalLimits X) (hu : CauchySeq u) : ∃ (m : ℕ → ℕ), StrictMono m ∧ ∀ (n : ℕ), dist (u (m n)) (u (m (n + 1))) < (1 / 2) ^ (n + 2)

Helper for Theorem 1.4: extract a geometric subsequence of a Cauchy sequence in the completion.

theorem helperForTheorem_1_4_diagonal_index (X : Type u) [MetricSpace X] {u : ℕ → CompletionViaFormalLimits X} {m : ℕ → ℕ} {x : ℕ → FormalLimit X} (hx : ∀ (n : ℕ), u (m n) = ⟦x n⟧) (hsmall : ∀ (n : ℕ), dist (u (m n)) (u (m (n + 1))) < (1 / 2) ^ (n + 2)) : ∃ (k : ℕ → ℕ), Monotone k ∧ (∀ (n j : ℕ), j ≥ k n → dist (↑(x n) j) (↑(x (n + 1)) j) < (1 / 2) ^ (n + 2)) ∧ ∀ (n j : ℕ), j ≥ k n → dist (↑(x (n + 1)) (k n)) (↑(x (n + 1)) j) < (1 / 2) ^ (n + 2)

Helper for Theorem 1.4: build a monotone diagonal index with pointwise control.

theorem helperForTheorem_1_4_diagonal_cauchy (X : Type u) [MetricSpace X] {x : ℕ → FormalLimit X} {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)) : CauchySeq fun (n : ℕ) => ↑(x n) (k n)

Helper for Theorem 1.4: the diagonal sequence is Cauchy.

theorem helperForTheorem_1_4_tendsto_of_cauchy_of_subseq {X : Type u} [MetricSpace X] {u : ℕ → X} (hu : CauchySeq u) {m : ℕ → ℕ} (hm : StrictMono m) {a : X} (hsub : Filter.Tendsto (fun (n : ℕ) => u (m n)) Filter.atTop (nhds a)) : Filter.Tendsto u Filter.atTop (nhds a)

Helper for Theorem 1.4: a Cauchy sequence with a convergent subsequence converges.