tendsto_limUnder

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#CauchySeq.tendsto_limUnder

← MathLib Explorer

English

A Cauchy sequence has a limit under limUnder with atTop.

Русский

Cauchy-последовательность имеет предел в limUnder при atTop.

LaTeX

$$$\\text{Tendsto}(u, atTop, nhds(limUnder atTop\\ u))$$$

Lean4

theorem tendsto_limUnder [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) :
    haveI := h.1.nonempty;
    Tendsto u atTop (𝓝 <| limUnder atTop u) :=
  h.le_nhds_lim

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru