Zulip Chat Archive

Stream: maths

Topic: Easy topological space question


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:03):

I wanted to use mem_nhds_of_is_topological_basis

view this post on Zulip 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 :=...

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:03):

but I am now sucked into some nonsense regarding filters

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:05):

which should be trivial

view this post on Zulip Mario Carneiro (Apr 02 2018 at 01:05):

use mem_nhds_sets

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:06):

no suggestions

view this post on Zulip Mario Carneiro (Apr 02 2018 at 01:06):

it's in analysis.topology.topological_space

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:07):

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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:08):

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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 01:18):

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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:18):

Why is anything non-trivial in the root namespace?

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:19):

Won't there be trouble ahead?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:19):

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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 01:20):

But here you can't even avoid it?

view this post on Zulip 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