Documentation Verification Report

AsLimit

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

Statistics

Metric	Count
Definitions `asLimit`, `asLimitCone`, `asLimitConeIso`, `diagram`, `fintypeDiagram`, `isoAsLimitConeLift`, `lim`	7
Theorems `isIso_asLimitCone_lift`	1
Total	8

Profinite

Definitions

Name	Category	Theorems
`asLimit` 📖	CompOp	—
`asLimitCone` 📖	CompOp	5 math math: `LightProfinite.lightToProfinite_map_proj_eq`, `instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`, `Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp`, `Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `isIso_asLimitCone_lift`
`asLimitConeIso` 📖	CompOp	—
`diagram` 📖	CompOp	4 math math: `LightProfinite.lightToProfinite_map_proj_eq`, `instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`, `Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `isIso_asLimitCone_lift`
`fintypeDiagram` 📖	CompOp	1 math math: `Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp`
`isoAsLimitConeLift` 📖	CompOp	—
`lim` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_asLimitCone_lift` 📖	mathematical	—	`CategoryTheory.IsIso` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Limits.Cone.pt` `DiscreteQuotient` `CompHausLike.toTop` `Preorder.smallCategory` `PartialOrder.toPreorder` `DiscreteQuotient.instPartialOrder` `diagram` `asLimitCone` `limitCone` `CategoryTheory.Limits.IsLimit.lift` `limitConeIsLimit`	—	`CompHausLike.isIso_of_bijective` `DiscreteQuotient.eq_of_forall_proj_eq` `CompHausLike.is_hausdorff` `CompHausLike.is_compact` `instTotallyDisconnectedSpaceCarrierToTop` `DiscreteQuotient.exists_of_compat` `Subtype.prop`

---

← Back to Index