Theorem Ordinal.isOpen_singleton_iff

Modification history