Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-16 18:01 066a168d

View on Github →

feat(topology/G_delta): add lemmas, minor golf (#9742)

the complement to a countable set is a Gδ set;
a closed set is a Gδ set;
finite union of Gδ sets is a Gδ set;
generalize some universe levels in topology.basic;
golf a few proofs in topology.uniform_space.basic;
add filter.has_basis.bInter_bUnion_ball.

Estimated changes

Modified src/topology/G_delta.lean

added theorem finset.is_Gδ_compl

modified theorem is_Gδ_Inter

added theorem is_Gδ_bUnion

added theorem is_Gδ_compl_singleton

modified theorem is_Gδ_empty

modified theorem is_Gδ_set_of_continuous_at

modified theorem is_Gδ_univ

added theorem is_closed.is_Gδ'

added theorem is_closed.is_Gδ

added theorem set.countable.is_Gδ_compl

added theorem set.finite.is_Gδ_compl

added theorem set.subsingleton.is_Gδ_compl

Modified src/topology/basic.lean

modified theorem mem_closure_iff_nhds_basis'

modified theorem mem_closure_iff_nhds_basis

Modified src/topology/uniform_space/basic.lean

added theorem filter.has_basis.bInter_bUnion_ball

modified theorem nhds_basis_uniformity'

modified theorem nhds_basis_uniformity