Def compHausToCondensed'

Modification history

2024-06-07 13:10

Mathlib/Condensed/Functors.lean

feat(Condensed): functor from light profinite sets to light condensed sets (#13502)

Modified compHausToCondensed'View on Github →

2023-11-15 18:03

Mathlib/Condensed/Functors.lean

feat(Condensed): functors from test objects to condensed sets (#8236) …

Added compHausToCondensed'View on Github →