## Stream: maths

### Topic: Understanding the definition of nhds

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

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

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

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

#### Scott Morrison (Jul 25 2020 at 06:31):

We only want sets containing an open set around a.

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

#### Jalex Stark (Jul 25 2020 at 07:14):

filters are not so popular outside of formalization

#### Jalex Stark (Jul 25 2020 at 07:14):

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

#### Jalex Stark (Jul 25 2020 at 07:14):

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

#### Jalex Stark (Jul 25 2020 at 07:15):

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

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

#### Chris Wong (Jul 25 2020 at 07:18):

That undergrad analysis course is rushing back to me now

#### Chris Wong (Jul 25 2020 at 07:20):

Thanks everyone for the help :grinning_face_with_smiling_eyes:

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

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