Theorems · Definition · category theory
CondensedSet
Type (u + 2)
Condensed sets (types) with the appropriate universe levels, i.e. Type (u + 1)-valued
sheaves on CompHaus.{u}.
- Defined in
- Mathlib.Condensed.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Condensedproof · cited by 20
Cited by44
Results whose statement or proof uses this declaration.
- CondensedSet.toTopCatstatement and proof · cited by 5
- TopCat.toCondensedSetstatement · cited by 3
- CondensedSet.LocallyConstant.functorstatement · cited by 3
- condensedSetToTopCatstatement and proof · cited by 2
- CondensedSet.toTopCatMapstatement and proof · cited by 2
- CondensedSet.LocallyConstant.adjunctionstatement · cited by 2
- Condensed.forgetstatement · cited by 2
- CondensedMod.isDiscrete_iff_isDiscrete_forgetstatement · cited by 1
- CondensedSet.isDiscrete_tfaestatement and proof · cited by 1
- CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCoconestatement and proof · cited by 1
- CondensedSet.topCatAdjunctionUnitstatement and proof · cited by 1
- Condensed.lanCondensedSetstatement · cited by 0