# Zulip Chat Archive

## Stream: maths

### Topic: Easy topological space question

#### Kevin Buzzard (Apr 02 2018 at 01:02):

I've been struggling on this one for about an hour :-/ I have a topological space X and an open set U and a basis B for the topology. I have x in U, and I simply want to find V in B with x in V and V in U.

#### Kevin Buzzard (Apr 02 2018 at 01:03):

I wanted to use `mem_nhds_of_is_topological_basis`

#### Kevin Buzzard (Apr 02 2018 at 01:03):

```
lemma mem_nhds_of_is_topological_basis {a : α} {s : set α} {b : set (set α)}
(hb : is_topological_basis b) : s ∈ (nhds a).sets ↔ ∃t∈b, a ∈ t ∧ t ⊆ s :=...
```

#### Kevin Buzzard (Apr 02 2018 at 01:03):

but I am now sucked into some nonsense regarding filters

#### Kevin Buzzard (Apr 02 2018 at 01:04):

So I would be done if I could prove that for U open and x in U, `U ∈ (nhds x).sets`

#### Kevin Buzzard (Apr 02 2018 at 01:05):

which should be trivial

#### Mario Carneiro (Apr 02 2018 at 01:05):

use `mem_nhds_sets`

#### Kevin Buzzard (Apr 02 2018 at 01:06):

no suggestions

#### Mario Carneiro (Apr 02 2018 at 01:06):

it's in `analysis.topology.topological_space`

#### Kevin Buzzard (Apr 02 2018 at 01:07):

oh but it's not topological_space.mem_nhds_sets :-)

#### Kevin Buzzard (Apr 02 2018 at 01:08):

works :-) Thanks! What's that doing in the root namespace?

#### Mario Carneiro (Apr 02 2018 at 01:18):

`nhds`

is in the root namespace, so so are its lemmas

#### Kevin Buzzard (Apr 02 2018 at 01:18):

Why is anything non-trivial in the root namespace?

#### Kevin Buzzard (Apr 02 2018 at 01:19):

Won't there be trouble ahead?

#### Kevin Buzzard (Apr 02 2018 at 01:19):

I import some topology module and all of a sudden there's extra stuff in the root namespace? I thought that that was some sort of disaster in CS

#### Kevin Buzzard (Apr 02 2018 at 01:19):

Isn't that exactly why python tells you not to do crazy `import *`

sort of things?

#### Kevin Buzzard (Apr 02 2018 at 01:20):

But here you can't even avoid it?

#### Mario Carneiro (Apr 02 2018 at 01:23):

Many basic structures are in the root namespace. But moving things around is not too painful, so we can adjust later if it becomes a problem

Last updated: May 12 2021 at 06:14 UTC