Commit 2020-06-23 17:15 26918a05

View on Github →

feat(topology/metric_space/baire): define filter residual (#3149) Fixes #2265. Also define a typeclass countable_Inter_filter and prove that both residual and μ.ae have this property.

Estimated changes

Modified src/analysis/normed_space/banach.lean

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.ae_ball_iff

Created src/order/filter/countable_Inter.lean

added theorem countable_Inter_mem_sets

added theorem countable_bInter_mem_sets

added theorem countable_sInter_mem_sets

added theorem eventually_countable_ball

added theorem eventually_countable_forall

Modified src/topology/basic.lean

added theorem dense_inter_of_open_left

added theorem dense_inter_of_open_right

Modified src/topology/instances/ennreal.lean

added theorem emetric.is_closed_ball

Modified src/topology/metric_space/baire.lean

added theorem eventually_residual

added theorem mem_residual

added def residual

Modified src/topology/metric_space/basic.lean

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.nhds_basis_closed_eball