Limits

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

Statistics

Metric	Count
Definitions	0
Theorems extremallyDisconnected_preimage, extremallyDisconnected_pullback, instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier, instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier	4
Total	4

Stonean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extremallyDisconnected_preimage 📖	mathematical	Topology.IsOpenEmbedding TopCat.str CompHausLike.toTop ExtremallyDisconnected TopCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom Stonean CompHausLike.category ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory	ExtremallyDisconnected Set.Elem Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom Stonean CompHausLike.category TopCat.carrier TopCat.str ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory Set.range instTopologicalSpaceSubtype Set Set.instMembership	—	IsClosed.preimage ContinuousMap.continuous IsCompact.isClosed CompHausLike.is_hausdorff isCompact_range CompHausLike.is_compact IsOpen.preimage Topology.IsOpenEmbedding.isOpen_range Set.preimage_image_eq Subtype.coe_injective Topology.IsClosedEmbedding.closure_image_eq IsClosed.isClosedEmbedding_subtypeVal isOpen_induced ExtremallyDisconnected.open_closure instExtremallyDisconnectedCarrierToTop Topology.IsOpenEmbedding.isOpenMap IsOpen.isOpenEmbedding_subtypeVal
extremallyDisconnected_pullback 📖	mathematical	Topology.IsOpenEmbedding TopCat.str CompHausLike.toTop ExtremallyDisconnected TopCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom Stonean CompHausLike.category ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory	ExtremallyDisconnected Set.Elem TopCat.carrier CompHausLike.toTop TopCat.str setOf DFunLike.coe CategoryTheory.ConcreteCategory.hom Stonean CompHausLike.category ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd	—	extremallyDisconnected_preimage ContinuousMap.continuous_toFun Topology.IsOpenEmbedding.isEmbedding CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits CategoryTheory.Limits.hasPullback_symmetry extremallyDisconnected_of_homeo
instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier 📖	mathematical	—	CompHausLike.HasExplicitFiniteCoproducts ExtremallyDisconnected TopCat.carrier TopCat.str	—	instExtremallyDisconnected instExtremallyDisconnectedCarrierToTop
instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier 📖	mathematical	—	CompHausLike.HasExplicitPullbacksOfInclusions ExtremallyDisconnected TopCat.carrier TopCat.str instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier	—	CompHausLike.hasPullbacksOfInclusions instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier extremallyDisconnected_pullback

---

← Back to Index