Zulip Chat Archive

Stream: maths

Topic: le_nhds_of_cauchy_adhp


view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 21:02):

What does adhp stand for in this name?

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 21:03):

lemma le_nhds_of_cauchy_adhp {f : filter α} {x : α} (hf : cauchy f)
  (adhs : f  𝓝 x  ) : f  𝓝 x

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 22:27):

adherence is French for closure I think? Did Patrick write the lemma?

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:13):

adherent point, I would guess

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:13):

I've also heard this called a cluster point, if I'm not mistaken

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:14):

https://en.wikipedia.org/wiki/Filter_(mathematics)#Clustering

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:16):

Moreover, every cluster point of a Cauchy filter is a limit point.

I think this is the lemma in question

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:19):

That is the kind of sentence I would like to see as leandoc on the theorem

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 23:32):

Thank you for the explanation. I'll PR a docstring together with my simplification of the proof.

view this post on Zulip Patrick Massot (Nov 30 2019 at 10:01):

I didn't write that lemma, but the name definitely stands for "adherent point". I don't think anyone cares strongly about that name. Yury's struggle proves that we need at least a good docstring, maybe a better name if someone finds one.


Last updated: May 14 2021 at 19:21 UTC