Limits

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

Statistics

Metric	Count
Definitions isTerminalPUnit	1
Theorems instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology	2
Total	3

LightProfinite

Definitions

Name	Category	Theorems
isTerminalPUnit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology 📖	mathematical	—	CompHausLike.HasExplicitFiniteCoproducts TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	instTotallyDisconnectedSpaceSigma instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology TopologicalSpace.instSecondCountableTopologySigmaOfCountable Finite.to_countable instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace
instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology 📖	mathematical	—	CompHausLike.HasExplicitPullbacks TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology	—	Subtype.totallyDisconnectedSpace Prod.totallyDisconnectedSpace instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology TopologicalSpace.Subtype.secondCountableTopology TopologicalSpace.instSecondCountableTopologyProd instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace

---

← Back to Index