Commit 2024-07-20 19:54 e66efa10

View on Github →

feat(Topology): define compactly generated topological spaces (#14508)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/CompactlyGenerated.lean

added def CompactlyGenerated.compactlyGeneratedToTop

added def CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTop

added def CompactlyGenerated.homeoOfIso

added def CompactlyGenerated.isoEquivHomeo

added def CompactlyGenerated.isoOfHomeo

added def CompactlyGenerated.of

added structure CompactlyGenerated

added def TopologicalSpace.compactlyGenerated

added theorem continuous_from_compactlyGenerated

added theorem continuous_from_compactlyGeneratedSpace

added theorem eq_compactlyGenerated