Nested intervals

Stream: Is there code for X?

[Jiatong Yang]

Is there code for the principle of nested intervals?
(A sequence of decreasing closed intervals of R has at least one point in common)

[Adam Topaz]

docs#is_compact.nonempty_Inter_of_directed_nonempty_compact_closed

[Adam Topaz]

Or the less general version where the family is indexed by the naturals:
docs#is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed

[Jiatong Yang]

Thank you very much!