Cauchy sequences #
A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality. There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.
Important definitions #
IsCauSeq: a predicate that says
f : ℕ → βis Cauchy.
CauSeq: the type of Cauchy sequences valued in type
βwith respect to an absolute value function
sequence, cauchy, abs val, absolute value
Given a Cauchy sequence
f with nonzero limit, create a Cauchy sequence with values equal to
the inverses of the values of