isCauSeq — Mathlib

English

In a normed field, CauSeq is equivalent to Cauchy sequences; Tendsto limit holds in both interpretations.

Русский

В нормированном поле CauSeq эквивалентно последовательностям Кау; существует предел и сходимость в обеих трактовках.

LaTeX

$$$ IsCauSeq(norm, u) \iff CauchySeq(u). $$$

Lean4

theorem isCauSeq {f : ℕ → β} (hf : CauchySeq f) : IsCauSeq norm f :=
  by
  obtain ⟨hf1, hf2⟩ := cauchy_iff.1 hf
  intro ε hε
  rcases hf2 {x | dist x.1 x.2 < ε} (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩
  simp only [mem_map, mem_atTop_sets, mem_preimage] at ht; obtain ⟨N, hN⟩ := ht
  exists N
  intro j hj
  rw [← dist_eq_norm]
  apply @htsub (f j, f N)
  apply Set.mk_mem_prod <;> solve_by_elim [le_refl]

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