Commit 2024-08-01 09:13 8de18835

View on Github →

feat(Topology): add API for compactly generated spaces (#15203) Define compactly generated topological spaces, which are spaces whose topology is coinduced by continuous maps whose domain is compact Hausdorff. Prove basic properties and instances. Provide instances for sequential spaces and Hausdorff weakly locally compact spaces.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/CompactlyGenerated.lean

deleted def TopologicalSpace.compactlyGenerated

deleted theorem continuous_from_compactlyGenerated

deleted theorem continuous_from_uCompactlyGeneratedSpace

deleted theorem eq_compactlyGenerated

deleted theorem uCompactlyGeneratedSpace_of_continuous_maps

Created Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

added theorem CompactlyGeneratedSpace.isClosed'

added theorem CompactlyGeneratedSpace.isClosed

added theorem CompactlyGeneratedSpace.isOpen'

added theorem CompactlyGeneratedSpace.isOpen

added def TopologicalSpace.compactlyGenerated

added theorem UCompactlyGeneratedSpace.isClosed

added theorem UCompactlyGeneratedSpace.isOpen

added theorem compactlyGeneratedSpace_of_coinduced

added theorem compactlyGeneratedSpace_of_continuous_maps

added theorem compactlyGeneratedSpace_of_isClosed

added theorem compactlyGeneratedSpace_of_isClosed_of_t2

added theorem compactlyGeneratedSpace_of_isOpen

added theorem compactlyGeneratedSpace_of_isOpen_of_t2

added theorem continuous_from_compactlyGenerated

added theorem continuous_from_compactlyGeneratedSpace

added theorem continuous_from_uCompactlyGeneratedSpace

added theorem eq_compactlyGenerated

added theorem uCompactlyGeneratedSpace_of_coinduced

added theorem uCompactlyGeneratedSpace_of_continuous_maps

added theorem uCompactlyGeneratedSpace_of_isClosed

added theorem uCompactlyGeneratedSpace_of_isOpen