Def CondensedSet.compactlyGeneratedAdjunctionCounitHomeo

Modification history

2024-07-29 07:19

Mathlib/Condensed/TopCatAdjunction.lean

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

Modified CondensedSet.compactlyGeneratedAdjunctionCounitHomeo View on Github →

2024-07-22 08:48

Mathlib/Condensed/TopCatAdjunction.lean

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

Added CondensedSet.compactlyGeneratedAdjunctionCounitHomeo View on Github →