equiv_lim — Mathlib

English

For every Cauchy sequence s, we have s equivalent to the constant sequence at its limit: s ≈ const abv (lim s).

Русский

Для каждой последовательности Коши s она эквивалентна константной последовательности с пределом: s ≈ const abv (lim s).

LaTeX

$$$s \\approx \\mathrm{const}(abv)\\, (\\lim s)$$$

Lean4

theorem equiv_lim (s : CauSeq β abv) : s ≈ const abv (lim s) :=
  Classical.choose_spec (complete s)

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