Easy topological space question

Stream: maths

[Kevin Buzzard]

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]

I wanted to use mem_nhds_of_is_topological_basis

[Kevin Buzzard]

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]

but I am now sucked into some nonsense regarding filters

[Kevin Buzzard]

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

[Kevin Buzzard]

which should be trivial

[Mario Carneiro]

use mem_nhds_sets

[Kevin Buzzard]

no suggestions

[Mario Carneiro]

it's in analysis.topology.topological_space

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

nhds is in the root namespace, so so are its lemmas

[Kevin Buzzard]

Why is anything non-trivial in the root namespace?

[Kevin Buzzard]

Won't there be trouble ahead?

[Kevin Buzzard]

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]

Isn't that exactly why python tells you not to do crazy import * sort of things?

[Kevin Buzzard]

But here you can't even avoid it?

[Mario Carneiro]

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