Theorem isOpen_setOf_disjoint_nhds_nhds

Modification history