Commit 2024-07-22 08:48 d9566d60

View on Github →

feat(Condensed): the fully faithful embedding of compactly generated topological spaces in condensed sets (#14514)

Estimated changes

Modified Mathlib/Condensed/TopCatAdjunction.lean

added def CondensedSet.compactlyGeneratedAdjunctionCounitHomeo

added def CondensedSet.condensedSetToCompactlyGenerated

added theorem CondensedSet.continuous_coinducingCoprod

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Topology/Category/CompactlyGenerated.lean

added theorem compactlyGeneratedSpace_of_continuous_maps