[Merged by Bors] - chore(Topology/Compactness/CountablyCompact): generalize theorem#39600

plp127 wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

plp127:aliu/inducing-freeplp127/mathlib4:aliu/inducing-freeCopy head branch name to clipboard