Commit 2025-06-03 15:37 8de95f8d

feat: a weaker definition of compactly generated spaces (#21237) This PR defines compactly coherent spaces as a topological space where a set is open iff its intersection with every compact set is open in that compact set. This notion is typically called compactly generated in the literature. There is a different definition of compactly generated spaces already in mathlib but that definition is stronger than the one presented here. They do however agree on Hausdorff spaces. See this wikipedia page for an explanation for the three different definitions of compactly generated spaces used in literature.