mathlib3

b9e46fe1 - refactor(topology): fix definition of residual (#18962)

refactor(topology): fix definition of residual (#18962) The current definition of `residual` in mathlib is incorrect for non-Baire spaces. This fixes it. Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>