Theorem continuous_from_uCompactlyGeneratedSpace

Modification history

2024-08-01 09:13

Mathlib/Topology/Category/CompactlyGenerated.lean

feat(Topology): add API for compactly generated spaces (#15203) …

Modified continuous_from_uCompactlyGeneratedSpace View on Github →

2024-07-29 07:19

Mathlib/Topology/Category/CompactlyGenerated.lean

feat: Rename `CompactlyGeneratedSpace` to `UCompactlyGeneratedSpace` (#15201) …

Added continuous_from_uCompactlyGeneratedSpace View on Github →