eventually_eventually — Mathlib

English

Shifting a Cauchy sequence by a fixed index preserves the Cauchy property, and conversely.

Русский

Смещение Коши-последовательности на фиксированное число сохраняет свойство Коши, и наоборот.

LaTeX

$$$\\forall k,\\ CauchySeq(u) \\iff CauchySeq(n\\mapsto u(n+k)).$$$

Lean4

theorem eventually_eventually [Preorder β] {u : β → α} (hu : CauchySeq u) {V : Set (α × α)} (hV : V ∈ 𝓤 α) :
    ∀ᶠ k in atTop, ∀ᶠ l in atTop, (u k, u l) ∈ V :=
  eventually_atTop_curry <| hu.tendsto_uniformity hV

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