cauchySeq_iff_tendsto_dist_atTop_0

English

A sequence u indexed by β is Cauchy if and only if the pairwise distances dist(u(n1), u(n2)) tend to 0 as (n1,n2) go to the top from β×β.

Русский

Последовательность {u} является фундаментальной (Коши) тогда и только тогда, когда расстояния между ее двумя точками стремятся к 0 при параллельном росте индексов.

LaTeX

$$$\\text{CauchySeq}(u) \\iff \\mathrm{Tendsto}\\big( (n,m) \\mapsto \\operatorname{dist}(u(n),u(m)) \\big)\\;\\text{atTop} \\; (\\mathcal{N}(0))$$$

Lean4

theorem cauchySeq_iff_tendsto_dist_atTop_0 [Nonempty β] [SemilatticeSup β] {u : β → α} :
    CauchySeq u ↔ Tendsto (fun n : β × β => dist (u n.1) (u n.2)) atTop (𝓝 0) :=
  by
  rw [cauchySeq_iff_tendsto, Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff, Function.comp_def]
  simp_rw [Prod.map_fst, Prod.map_snd]

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