Theorem contDiffOn_of_locally_contDiffOn

Modification history