Commit 2023-11-15 18:03 e0e141f7

View on Github →

feat(Condensed): functors from test objects to condensed sets (#8236) We define the natural functor CompHaus ⥤ CondensedSet and its friends for profinite and Stonean spaces.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Condensed/Basic.lean

Created Mathlib/Condensed/Functors.lean

added def Condensed.ulift

added def compHausToCondensed'

added def compHausToCondensed

added def profiniteToCondensed

added def stoneanToCondensed