open interval in nonempty open set

Stream: Is there code for X?

[Jeremy Avigad]

I have a nonempty open set in the reals. How do I prove that there exists an open interval contained in it?

[Yaël Dillies]

This boils down to the fact that open intervals of reals form a filter basis for the topology. Trying to piece up the elements now...

[Floris van Doorn]

docs#mem_nhds_iff_exists_Ioo_subset (combined with docs#is_open.mem_nhds) gets you there.

[Floris van Doorn]

docs#is_open.exists_Ioo_subset gets you there in one step :-)