Zulip Chat Archive

Stream: maths

Topic: Understanding the definition of nhds


view this post on Zulip Chris Wong (Jul 25 2020 at 06:02):

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?

view this post on Zulip Johan Commelin (Jul 25 2020 at 06:03):

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

view this post on Zulip Chris Wong (Jul 25 2020 at 06:27):

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.

view this post on Zulip Chris Wong (Jul 25 2020 at 06:30):

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

view this post on Zulip Scott Morrison (Jul 25 2020 at 06:31):

We only want sets containing an open set around a.

view this post on Zulip Chris Wong (Jul 25 2020 at 07:10):

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:

view this post on Zulip Jalex Stark (Jul 25 2020 at 07:14):

filters are not so popular outside of formalization

view this post on Zulip Jalex Stark (Jul 25 2020 at 07:14):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 07:14):

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

view this post on Zulip Jalex Stark (Jul 25 2020 at 07:15):

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

view this post on Zulip Chris Wong (Jul 25 2020 at 07:17):

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.

view this post on Zulip Chris Wong (Jul 25 2020 at 07:18):

That undergrad analysis course is rushing back to me now

view this post on Zulip Chris Wong (Jul 25 2020 at 07:20):

Thanks everyone for the help :grinning_face_with_smiling_eyes:

view this post on Zulip Anatole Dedecker (Jul 25 2020 at 10:16):

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

view this post on Zulip Chris Wong (Jul 25 2020 at 11:22):

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


Last updated: May 10 2021 at 08:14 UTC