Naming Suslin Spaces

Stream: mathlib4

[Lara Toledano]

As part of the ongoing work to add the proof of the Effros Theorem to mathlib (see #mathlib4 > Effros Theorem), I would like to add a class for the topological spaces such that MeasureTheory.AnalyticSet Set.univ.

I opened #32742 with the first try for SuslinSpace, see also wikipedia, however I feel it would probably be best to stay clear of proper nouns and use a more descriptive identifier. I believe something like AnalyticSpace would be good. @Anatole Dedecker suggested IsAnalytic/AnalyticSpace among others.

One issue with this name is that there is already an unrelated concept of algebraic geometry, see https://en.wikipedia.org/wiki/Analytic_space. I feel like there is very little risk of confusion, as long as AnalyticSpace lives in a relevant namespace, for instance MeasureTheory or MeasureTheory.AnalyticSet.

Descriptive set theory is actually not my area of expertise. Is anyone familiar with the common practice there?

[James E Hanson]

In descriptive set theory and mathematical logic, the term 'analytic space' is standard and the only context I'm aware of in which 'Suslin space' shows up is certain kinds of generalized descriptive set theory in which Suslin sets are no longer the same thing as analytic sets.

'Suslin space' might be more common in some parts of the measure theory literature, but I'm not as familiar with that.