Topic: cau_seq, cauchy_seq
Yury G. Kudryashov (Nov 29 2019 at 02:17):
Hi, what is the reason to introduce
cau_seq in mathlib? When I first tried to understand what happens, presence of both
cauchy_seq was really confusing. I can see that it makes some definitions computable but I don't think that
cau_seq lead to any reasonable computable definitions. I mean, a computable Cauchy sequence without a computable estimate on the rate of convergence gives no information about the limit.
Mario Carneiro (Nov 29 2019 at 03:12):
It is a bootstrapping thing.
cau_seq does not rely on any topology for its definition, but it is superceded by
Last updated: May 06 2021 at 19:30 UTC