feat(Topology/GDelta): a completely metrizable subspace of a T6 space is Gδ - #42912

feat(Topology/GDelta): a completely metrizable subspace of a T6 space is Gδ#42912

justin-palumbo wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justin-palumbo:feature-gdelta-completely-metrizablejustin-palumbo/mathlib4:feature-gdelta-completely-metrizableCopy head branch name to clipboard