Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-11 04:03 11117ec5

View on Github →

feat(topology/G_delta): a finite set is a Gδ-set (#9644)

Estimated changes

Modified src/topology/G_delta.lean

added theorem is_Gδ_empty

added theorem is_Gδ_singleton

added theorem set.finite.is_Gδ

Modified src/topology/separation.lean

added theorem bInter_basis_nhds