lim — Mathlib

English

The limit of a Cauchy sequence in a complete ring β with abv is defined noncomputably as a chosen representative limit in β.

Русский

Предел последовательности Коши в полной группе β по abv определён невычислимым способом как выбранный предел в β.

LaTeX

$$$\\lim: CauSeq\\;\\beta\\;abv\\to\\beta$ с \\forall s:\\ CauSeq\\;\\beta\\;abv,\ \ s\\approx \\mathrm{const}(abv)\\,(\\lim s)$$$

Lean4

/-- The limit of a Cauchy sequence in a complete ring. Chosen non-computably. -/
noncomputable def lim (s : CauSeq β abv) : β :=
  Classical.choose (complete s)

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