def SeqConvergesTo {k : Type u_1} [SeminormedAddCommGroup k] (x : ℕ → k) (ℓ : k) : Prop

theorem seqConvergesTo_iff_forall_eps {k : Type u_1} [SeminormedAddCommGroup k] (x : ℕ → k) (ℓ : k) : SeqConvergesTo x ℓ ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, dist (x n) ℓ < ε

theorem seqConvergesTo_add {k : Type u_1} [NormedField k] {x y : ℕ → k} {a b : k} (hx : SeqConvergesTo x a) (hy : SeqConvergesTo y b) : SeqConvergesTo (x + y) (a + b)

def IsCauchySeq {k : Type u_1} [NormedField k] (x : ℕ → k) : Prop

theorem isCauchySeq_iff_cauchySeq {k : Type u_1} [NormedField k] (x : ℕ → k) : IsCauchySeq x ↔ CauchySeq x

theorem convergent_imp_cauchy {k : Type u_1} [NormedField k] {x : ℕ → k} {ℓ : k} (hx : SeqConvergesTo x ℓ) : CauchySeq x

def SeqEquiv {k : Type u_1} [SeminormedAddCommGroup k] (a b : ℕ → k) : Prop

theorem seqEquiv_iff_forall_eps_norm {k : Type u_1} [SeminormedAddCommGroup k] (a b : ℕ → k) : SeqEquiv a b ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ‖a n - b n‖ < ε

def IsCompleteField (k : Type u_2) [NormedField k] : Prop

theorem dense_iff_forall_norm_sub_lt {k : Type u_1} [NormedField k] {S : Set k} : Dense S ↔ ∀ (x : k), ∀ ε > 0, ∃ y ∈ S, ‖x - y‖ < ε

@[reducible, inline]

abbrev NormedFieldCompletion (k : Type u_1) [NormedField k] : Type u_1

@[implicit_reducible]

noncomputable instance NormedFieldCompletion.instField (k : Type u_1) [NormedField k] [CompletableTopField k] : Field (UniformSpace.Completion k)

@[implicit_reducible]

noncomputable instance NormedFieldCompletion.instNormedField (k : Type u_1) [NormedField k] [CompletableTopField k] : NormedField (UniformSpace.Completion k)

instance NormedFieldCompletion.instCompleteSpace (k : Type u_1) [NormedField k] : CompleteSpace (UniformSpace.Completion k)

noncomputable def completionEmbedding (k : Type u_2) [NormedField k] [CompletableTopField k] : k →+* UniformSpace.Completion k

theorem denseRange_completion_coe (k : Type u_1) [NormedField k] : DenseRange UniformSpace.Completion.coe'

noncomputable def completion_extensionHom (k : Type u_1) [NormedField k] [CompletableTopField k] (k' : Type u_2) [NormedField k'] [CompleteSpace k'] (f : k →+* k') (hf : Continuous ⇑f) : UniformSpace.Completion k →+* k'

theorem cauchy_seq_completion_equiv_from_k (k : Type u_1) [NormedField k] (z : ℕ → UniformSpace.Completion k) (hz : CauchySeq z) : ∃ (x : ℕ → k), (CauchySeq fun (n : ℕ) => ↑(x n)) ∧ SeqEquiv z fun (n : ℕ) => ↑(x n)