Theorem isOpen_iff_eventually

Modification history