Every point in an open subset of reals has an open interval

Stream: Is there code for X?

[Michael Novak]

Given an open subset of real numbers is there a theorem in Mathlib that says that for every point of the subset there is an open interval in the subset that contain the point? I managed to find a theorem that just says that there is an open interval (not containing a point) and also a general theorem that says that for every point in the subset there is a neighborhood, but I want specifically an open interval of the form Set.Ioo a b.

[Aaron Liu]

found docs#mem_nhds_iff_exists_Ioo_subset

[Aaron Liu]

just by searching @loogle Set.Ioo, Exists, nhds

[loogle]

:search: nhds_order_unbounded, mem_nhds_iff_exists_Ioo_subset, and 17 more

[Aaron Liu]

then you can use docs#IsOpen.mem_nhds

[Michael Novak]

Thank you very much!