Understanding the definition of nhds

Stream: maths

[Chris Wong]

I see that the neighborhood filter is defined as "the infimum of principal filters of open neighborhoods of a"
https://leanprover-community.github.io/mathlib_docs/topology/basic.html#nhds
What's the reason for the "infimum of principal filters" part? Would just "the open neighborhoods of a" be a filter as well?

[Johan Commelin]

See the 3rd theorem below it docs#le_nhds_iff or maybe docs#mem_nhds_sets_iff

[Chris Wong]

Interesting, thanks!

And I just answered my own question. The superset of an open set might not be open. So we need to bring in the supersets explicitly (i.e. take the principal filters) to satisfy the "upward closed" axiom. I guess the infimum is there for a similar reason, except for the intersection axiom instead.

[Chris Wong]

Now I'm wondering why we go through all this effort, instead of nhds a := { s | a ∈ s } ... :thinking:

[Scott Morrison]

We only want sets containing an open set around a.

[Chris Wong]

Right, and I guess having only open sets makes it easier to use the topology stuff.

Follow-up question -- if a filter contains all supersets, and some of the supersets of an open set are non-open, then how do we prevent these non-open sets from sneaking in?

I realize these questions are more about filters in general than Lean :sweat_smile:

[Jalex Stark]

filters are not so popular outside of formalization

[Jalex Stark]

the non-open sets aren't sneaking in, they're walking through the front door

[Jalex Stark]

this is what people in math departments usually mean when they say neighborhood

[Jalex Stark]

https://en.wikipedia.org/wiki/Neighbourhood_(mathematics)

[Chris Wong]

Ah right that makes sense now, thanks Jalex!
I misread Scott's comment. "A set (not necessarily open) that contains an open set around a" is indeed the definition of a neighborhood.

[Chris Wong]

That undergrad analysis course is rushing back to me now

[Chris Wong]

Thanks everyone for the help :grinning_face_with_smiling_eyes:

[Anatole Dedecker]

Would it be equivalent to define it as the filter generated by all open sets containing a ?

[Chris Wong]

I think so. nhds_basis_opens says that those sets form a basis.