Theorems · Definition · category theory
TopCat.toLightCondSet
TopCat → LightCondSet
Associate to a u-small topological space the corresponding light condensed set, given by
yonedaPresheaf.
- Defined in
- Mathlib.Condensed.Light.TopComparison
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCat.carrierproof · cited by 3,184
- TopCatstatement and proof · cited by 1,889
- SecondCountableTopologyproof · cited by 750
- TotallyDisconnectedSpaceproof · cited by 295
- LightCondSetstatement · cited by 26
- TopCat.toSheafCompHausLikeproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- LightCondSet.topCatAdjunctionCounitstatement and proof · cited by 1
- LightCondSet.topCatAdjunctionCounitEquivstatement · cited by 1
- LightCondSet.topCatAdjunctionUnitstatement · cited by 1
- LightCondSet.topCatAdjunctionCounit_bijectivestatement · cited by 0
- LightCondSet.topCatAdjunctionUnit_hom_appstatement · cited by 0
- LightCondSet.sequentialAdjunctionHomeostatement and proof · cited by 0