issue !4#2032: refactor: redefine metrizable and Polish s...

Stream: triage

[Random Issue Bot]

Today I chose issue 2032 for discussion!

refactor: redefine metrizable and Polish spaces
Created by @Yury G. Kudryashov (@urkud) on 2023-02-03
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Yury G. Kudryashov]

It's still on my TODO list but it's waiting for some reorganization of imports (e.g., moving definitions outside of more advanced files).

[Random Issue Bot]

Today I chose issue #2032 for discussion!

refactor: redefine metrizable and Polish spaces
Created by @Yury G. Kudryashov (@urkud) on 2023-02-03
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Johan Commelin]

Yury G. Kudryashov said:

It's still on my TODO list but it's waiting for some reorganization of imports (e.g., moving definitions outside of more advanced files).

Does this still apply? If so, can you please list (a representative sample) of definitions/files?

[Yury G. Kudryashov]

First, I need to reorganize imports so that MetrizableSpace is defined in a (new) file with minimal imports, then redefine it and move the definition before MetricSpace.

[Yury G. Kudryashov]

I'm sorry I neglected this for a long time. I have very little time for Mathlib because of my day job, and formalizing new math almost always takes priority over working on the tech debt.

[Yury G. Kudryashov]

I'll try to come up with a plan that can be done in a series of small PRs with well-defined scope, probably over the next weekend (I'm busy at my day job during the week).

[Johan Commelin]

@Yury G. Kudryashov If you can write the plan, then maybe others can help execute it :smiley:

[Johan Commelin]

I understand that you are busy, so I didn't mean to add pressure, but rather take some away...