feat: add standard Borel space class (#7243)

add a class `StandardBorelSpace`, whose relationship to `PolishSpace` is analogous to the relationship between `PolishSpace` and complete metric space. The usefulness is shown by `_root_.MeasurableSet.standardBorel`: A measurable subset of a standard Borel space is Polish. Note that a borel measurable subset of a Polish space will not typically be Polish in the induced topology!

Specific things done in this PR:

- added some basic instances for `StandardBorelSpace`
- changed theorems with hypotheses `[MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [PolishSpace X]` but which do not refer to the topology on `X` to depend instead on  `[MeasurableSpace X][StandardBorelSpace X]`. These automatically generalize the old theorems thanks to `standardBorel_of_polish`.

I believe this sort of refactoring can be pushed a lot farther in future PRs. 



Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>

Author: Felix-Weilacher