Theorem CompactlyCoherentSpace.of_isOpen_forall_compactSpace

Modification history

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