Polish Groups

Stream: Is there code for X?

[luna elliott]

Sorry I'm new. Is there any code on Polish group topologies? Also is there a better way to find out what has been done then searching it here: https://leanprover-community.github.io/mathlib4_docs/search.html?q=PolishGroup?

[Matt Diamond]

Have you taken a look at PolishSpace?

[luna elliott]

This looks like it contains a lot of lemmas I would want for Polish groups but as far as I can see doesn't talk about Polish groups specifically. Does this mean Polish groups have not been done in Lean yet? And if so would it make sense for me to try implementing them?

[Etienne Marion]

I guess a Polish group would be phrased as [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G]

[Etienne Marion]

@loogle PolishSpace, Group

[loogle]

:search: QuotientGroup.borelSpace, CosetSpace.borelSpace, and 7 more