Documentation
Mathlib
.
Condensed
.
CartesianClosed
Search
Google site search
return to top
source
Imports
Init
Mathlib.Condensed.Limits
Mathlib.CategoryTheory.Closed.Types
Mathlib.CategoryTheory.Sites.CartesianClosed
Imported by
instCartesianClosedCondensedSet
Condensed sets form a cartesian closed category
#
source
instance
instCartesianClosedCondensedSet
:
CategoryTheory.CartesianClosed
CondensedSet
Equations
instCartesianClosedCondensedSet
=
inferInstanceAs
(
CategoryTheory.CartesianClosed
(
CategoryTheory.Sheaf
(
CategoryTheory.coherentTopology
CompHaus
)
(Type
(?u.7 + 1)))
)