interior and ord_connected

Stream: Is there code for X?

[Yaël Dillies]

Do we know something along the lines of "The interior of an order connected set in a (dense?) linear order (with the order or order closed topology) is the set minus the eventual endpoints"?

[Kevin Buzzard]

I guess this isn't true for the naturals so one does need some kind of density argument

[Yaël Dillies]

Ahah! You don't actually need a density argument because order_closed_topology does it for you. See docs#is_open_Ioo along with docs#interior_Icc.

[Yaël Dillies]

Yeah okay, you do need densely_ordered.