## Stream: maths

#### Yury G. Kudryashov (Nov 29 2019 at 21:02):

What does adhp stand for in this name?

#### 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


#### Kevin Buzzard (Nov 29 2019 at 22:27):

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

#### Mario Carneiro (Nov 29 2019 at 23:13):

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

#### Mario Carneiro (Nov 29 2019 at 23:14):

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

#### 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

#### Mario Carneiro (Nov 29 2019 at 23:19):

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

#### 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.

#### 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