Commit 2023-05-20 16:28 b9e46fe1

View on Github →

refactor(topology): fix definition of residual (#18962) The current definition of residual in mathlib is incorrect for non-Baire spaces. This fixes it.

Estimated changes

Modified src/order/filter/countable_Inter.lean

added def filter.countable_generate

added theorem filter.countable_generate_is_greatest

added inductive filter.countable_generate_sets

added theorem filter.le_countable_generate_iff_of_countable_Inter_filter

added theorem filter.mem_countable_generate_iff

Modified src/topology/G_delta.lean

added theorem mem_residual_iff

added theorem residual_of_dense_Gδ

added theorem residual_of_dense_open

Modified src/topology/metric_space/baire.lean

modified theorem dense_of_mem_residual