Theorem Ordinal.isSuccLimit_of_mem_frontier

Modification history