Documentation

Mathlib.Condensed.CartesianClosed

Condensed sets form a Cartesian closed category #

source
🔸 coverage
@[implicit_reducible]
instance instCartesianMonoidalCategoryCondensedSet :
CategoryTheory.CartesianMonoidalCategory CondensedSet
source
🔸 coverage
@[implicit_reducible]
noncomputable instance instMonoidalClosedCondensedSet :
CategoryTheory.MonoidalClosed CondensedSet