Wrong definition of residual?

Stream: maths

[Felix Weilacher]

Currently docs#residual defines residual in its docstring as "contains a dense G-delta", and officially as the filter generated by such sets. It notes that these don't necessarily coincide in non Baire spaces.

In fact, as far as I can tell neither of these definitions agrees with the one I am used to (and the only one I could find in a brief search), which is that the residual sets are (the elements of) the countable_Inter_filter generated by dense opens.

This definition coincides with the other two in Baire spaces, but there are nontrivial things you can say about Baire category without assuming your space is Baire, and I don't know if they work with the current mathlib definition.

[Felix Weilacher]

Has anyone seen the mathlib or docstring definition anywhere? does it have a use? It doesn't seem as though mathlib ever mentions residual for non Baire spaces after the definition.

[Felix Weilacher]

Maybe @Sebastien Gouezel or someone else could take a look at #18962? It corrects the definition but for the most part does not touch the places it is used. I am not sure if changes in those places would be desired.

[Yury G. Kudryashov]

I defined this filter some time ago. I didn't care about non-Baire spaces. I'm happy with any definition that is equal to the current one in a Baire space.

[Yury G. Kudryashov]

My main goal was to be able to use filter notation to say things like docs#real.disjoint_residual_ae

[Yury G. Kudryashov]

It was defined in #3149.

[Felix Weilacher]

Yury G. Kudryashov said:

My main goal was to be able to use filter notation to say things like docs#real.disjoint_residual_ae

My PR preserves the type of residual a as filter a. The general definition of residual sets in a topological space is always a filter. There seems to have been a misunderstanding about this. "contains a dense G-delta" is not the general definition.

[Yury G. Kudryashov]

Left a review.