Theorems · Theorem · commutative algebra

CauSeq.IsComplete.isComplete

∀ {α : Type u_1} {inst : Field α} {inst_1 : LinearOrder α} {inst_2 : IsStrictOrderedRing α} {β : Type u_2}
  {inst_3 : Ring β} {abv : β → α} {inst_4 : IsAbsoluteValue abv} [self : CauSeq.IsComplete β abv] (s : CauSeq β abv),
  ∃ b, s ≈ CauSeq.const abv b

Every Cauchy sequence has a limit.

Defined in

Mathlib.Algebra.Order.CauSeq.Completion

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CauSeq.IsComplete