Limits

📁 Source: Mathlib/Topology/Category/Profinite/Limits.lean

Statistics

Metric	Count
Definitions isTerminalPUnit	1
Theorems instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier, instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier	2
Total	3

Profinite

Definitions

Name	Category	Theorems
isTerminalPUnit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier 📖	mathematical	—	CompHausLike.HasExplicitFiniteCoproducts TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	instTotallyDisconnectedSpaceSigma instTotallyDisconnectedSpaceCarrierToTop
instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier 📖	mathematical	—	CompHausLike.HasExplicitPullbacks TotallyDisconnectedSpace TopCat.carrier TopCat.str	—	Subtype.totallyDisconnectedSpace Prod.totallyDisconnectedSpace instTotallyDisconnectedSpaceCarrierToTop

---

← Back to Index