of_convergence — Mathlib

English

The convergents of the continued fraction expansion of v converge to v in the given topological space.

Русский

Сходимость последовательности ближайших приближений непрерывного разложения в топологическом пространстве сходится к v.

LaTeX

$$$\\mathrm{Tendsto}\\; (\\mathrm{of}\\;v).\\mathrm{convs}\\; \\mathrm{atTop} \\; (\\mathcal{N})\\; v.$$$

Lean4

theorem of_convergence [TopologicalSpace K] [OrderTopology K] : Filter.Tendsto (of v).convs Filter.atTop <| 𝓝 v := by
  simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v

Похожие утверждения