naming: nhds_iInf and Filter.nhds_iInf

Stream: mathlib4

[Eric Wieser]

docs#nhds_iInf is about the neigborhoods in an infimum of topologies, while docs#Filter.nhds_iInf is about the neighborhood of an infimum of points.

The naming here seems a little weird; filters are no more present in the former than the latter. Should one be in the TopologicalSpace namespace?

[Eric Wieser]

(This came up in #18178)

[Anatole Dedecker]

Eric Wieser said:

docs#Filter.nhds_iInf is about the neighborhood of an infimum of points.

This is even more specific: docs#Filter.nhds_iInf is a fact about the topology on the space of filters. I think the name is fine but it should be protected.

[Eric Wieser]

Ah whoops, you're quite right. I agree, the resolution here is just to protected it