Is neighborhood an open set?

Stream: mathlib4

[Yifan Bai]

Suppose s ∈ 𝓝 x, then is s an open set? I just found some theorems like isOpen_iff_mem_nhds, but it seems not what I want. I want to construct an open cover by using the neighborhoods around each point in a compact set, so that I could use the finite cover theorem.

[Daniel Weber]

No, see docs#mem_nhds_iff - the neighborhoods of a point are sets with an opening subset containing it, but they themselves don't have to be open (for a concrete example, [0, 1] is a neighborhood of 0.5 in the reals)

[Yifan Bai]

Daniel Weber said:

No, see docs#mem_nhds_iff - the neighborhoods of a point are sets with an opening subset containing it, but they themselves don't have to be open (for a concrete example, [0, 1] is a neighborhood of 0.5 in the reals)

Thank you, maybe I need to use mem_nhds_iff to choose an open set then.

[Daniel Weber]

See also docs#nhds_basis_opens

[Notification Bot]

This topic was moved here from #lean4 > Is neighborhood an open set? by Patrick Massot.

[Patrick Massot]

@Yifan Bai you should probably share your code. Very often people want open neighborhoods because they are taught to use theme everywhere, but any neighborhood would be good enough. For instance maybe in your case you could use IsCompact.elim_nhds_subcover_nhdsSet, but it’s hard to say without seeing your code. Maybe you do need open neighborhood and then we’ll be able to tell you how to get them very efficiently.

[Yifan Bai]

@Patrick Massot Because we are trying to write a scheme for a theorem's proof in lean, which is the uniform Kurdyka-Łojasiewicz property in nonconvex optimization theory, I'm just considering how to write the code properly and haven't begin to write the code. Kurdyka-Łojasiewicz property mainly tells that for any point in a set, there exists a neighborhood satisfying an inequality, and we want to use these neiborhoods to build a open cover, then use the finite cover theorems, which is used in the proof. Thanks for your remind of IsCompact.elim_nhds_subcover_nhdsSet, which I think it should be what we really want, because we won't use any properties of open sets.