le_nhds_of_cauchy_adhp

Stream: maths

[Yury G. Kudryashov]

What does adhp stand for in this name?

[Yury G. Kudryashov]

lemma le_nhds_of_cauchy_adhp {f : filter α} {x : α} (hf : cauchy f)
  (adhs : f ⊓ 𝓝 x ≠ ⊥) : f ≤ 𝓝 x

[Kevin Buzzard]

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

[Mario Carneiro]

adherent point, I would guess

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

I think this is the lemma in question

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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.