Commit 2024-01-31 18:47 fb969e7b

View on Github →

chore(ProperSpace): rename constructors (#10138) Rename properSpace_of_* to ProperSpace.of_*, restore old names as deprecated aliases. This affects:

  • properSpace_of_locallyCompactSpace -> ProperSpace.of_locallyCompactSpace, also golf using new ProperSpace.of_seq_closedBall;
  • properSpace_of_locallyCompact_module -> ProperSpace.of_locallyCompact_module;
  • properSpace_of_compact_closedBall_of_le -> ProperSpace.of_isCompact_closedBall_of_le, also changed compact -> isCompact in the name.

Estimated changes