Theorem CompactlyCoherentSpace.of_isOpen

Modification history

2025-06-03 15:37
Mathlib/Topology/Compactness/CompactlyCoherentSpace.lean
feat: a weaker definition of compactly generated spaces (#21237) …
Added CompactlyCoherentSpace.of_isOpenView on Github →