Zulip Chat Archive

Stream: maths

Topic: cau_seq, cauchy_seq


view this post on Zulip 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 cau_seq and 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.

view this post on Zulip 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 cauchy_seq


Last updated: May 06 2021 at 19:30 UTC