Commit 2023-09-08 11:01 2b261f6d

View on Github →

chore: implement porting notes about Polish spaces (#6991) Make the following changes which were intentionally left till after the port:

  • Move several instances of PolishSpace from MeasureTheory.Constructions.Polish to Topology.MetricSpace.Polish
  • Remove instance of PolishSpace for nat -> nat, since lean4 can find this automatically
  • Change PolishSpace to extend SecondCountableTopology, since lean4 now allows loops in TC inference.

Estimated changes

modified theorem IsClosed.polishSpace