Commit 2024-03-16 13:20 00106234

View on Github →

feat: better polishSpace_of_complete_second_countable (#10890)

  • Make it work for a UniformSpace with extra properties.
  • Use it to golf some instances.

Estimated changes

deleted def PolishSpace.AuxCopy
added theorem PolishSpace.t2Space