English
A CauSeq tends to its limit in a complete space; the limit is the limit of the sequence in the topology.
Русский
CauSeq стремится к пределу в полном пространстве; предел совпадает с математическим пределом последовательности.
LaTeX
$$$ \operatorname{Tendsto}(f)\; atTop \; (\mathcal{nhds}(f.lim)). $$$
Lean4
theorem tendsto_limit [NormedRing β] [hn : IsAbsoluteValue (norm : β → ℝ)] (f : CauSeq β norm)
[CauSeq.IsComplete β norm] : Tendsto f atTop (𝓝 f.lim) :=
tendsto_nhds.mpr
(by
intro s os lfs
suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ hε
exists N
intro b hb
apply hεs
dsimp [Metric.ball]
rw [dist_comm, dist_eq_norm]
solve_by_elim)
