TopComparison

📁 Source: Mathlib/Condensed/Light/TopComparison.lean

Statistics

Metric	Count
Definitions toLightCondSet, topCatToLightCondSet	2
Theorems	0
Total	2

TopCat

Definitions

Name	Category	Theorems
toLightCondSet 📖	CompOp	3 math math: LightCondSet.topCatAdjunctionUnit_val_app_apply, LightCondSet.topCatAdjunctionCounit_bijective, LightCondSet.topCatAdjunctionUnit_val_app

(root)

Definitions

Name	Category	Theorems
topCatToLightCondSet 📖	CompOp	4 math math: LightCondSet.instFaithfulTopCatTopCatToLightCondSet, LightCondSet.instEpiTopCatAppCounitTopCatAdjunction, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom

---

← Back to Index