cauchySeq_iff — Mathlib

English

If (𝓤 α) has a basis with p and s, then CauchySeq u is equivalent to existence of N with certain membership conditions.

Русский

Если у 𝓤 α есть базис с p и s, то CauchySeq u эквивалентно существованию N с определенными условиями принадлежности.

LaTeX

$$$\\text{HasBasis}(p,s) \\Rightarrow \\text{CauchySeq}(u) \\iff \\forall i, p(i) \\Rightarrow \\exists N, \\forall n \\ge N, (u(n),u(N))\\in s(i).$$$

Lean4

theorem cauchySeq_iff {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V := by
  simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

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