Documentation Verification Report

Explicit

📁 Source: Mathlib/Condensed/Explicit.lean

Statistics

Metric	Count
Definitions `ofSheafCompHaus`, `ofSheafForgetCompHaus`, `ofSheafForgetProfinite`, `ofSheafForgetStonean`, `ofSheafProfinite`, `ofSheafStonean`, `ofSheafCompHaus`, `ofSheafProfinite`, `ofSheafStonean`, `ofSheafCompHaus`, `ofSheafProfinite`, `ofSheafStonean`	12
Theorems `equalizerCondition`, `equalizerCondition_profinite`, `instPreservesFiniteProductsOppositeCompHausVal`, `instPreservesFiniteProductsOppositeProfiniteVal`, `instPreservesFiniteProductsOppositeStoneanVal`	5
Total	17

Condensed

Definitions

Name	Category	Theorems
`ofSheafCompHaus` 📖	CompOp	—
`ofSheafForgetCompHaus` 📖	CompOp	—
`ofSheafForgetProfinite` 📖	CompOp	—
`ofSheafForgetStonean` 📖	CompOp	—
`ofSheafProfinite` 📖	CompOp	—
`ofSheafStonean` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equalizerCondition` 📖	mathematical	—	`CategoryTheory.regularTopology.EqualizerCondition` `CompHaus` `CompHausLike.category` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `CompHaus.instHasPropTrue` `CategoryTheory.Sheaf.cond`
`equalizerCondition_profinite` 📖	mathematical	—	`CategoryTheory.regularTopology.EqualizerCondition` `Profinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `Profinite.instHasPropTotallyDisconnectedSpaceCarrier` `Subtype.totallyDisconnectedSpace` `Prod.totallyDisconnectedSpace` `Profinite.instTotallyDisconnectedSpaceCarrierToTop` `CategoryTheory.Sheaf.cond`
`instPreservesFiniteProductsOppositeCompHausVal` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `CompHaus.instHasPropTrue` `CategoryTheory.Sheaf.cond`
`instPreservesFiniteProductsOppositeProfiniteVal` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `Profinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier` `Profinite.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition` `CompHausLike.instHasLimitWalkingCospanCospan` `Profinite.instHasPropTotallyDisconnectedSpaceCarrier` `Subtype.totallyDisconnectedSpace` `Prod.totallyDisconnectedSpace` `Profinite.instTotallyDisconnectedSpaceCarrierToTop` `CategoryTheory.Sheaf.cond`
`instPreservesFiniteProductsOppositeStoneanVal` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `Opposite` `Stonean` `CategoryTheory.Category.opposite` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier` `Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier` `Stonean.instPreregular`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier` `Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier` `Stonean.instPreregular` `CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective` `Stonean.instProjective` `CategoryTheory.Sheaf.cond`

CondensedMod

Definitions

Name	Category	Theorems
`ofSheafCompHaus` 📖	CompOp	—
`ofSheafProfinite` 📖	CompOp	—
`ofSheafStonean` 📖	CompOp	—

CondensedSet

Definitions

Name	Category	Theorems
`ofSheafCompHaus` 📖	CompOp	—
`ofSheafProfinite` 📖	CompOp	—
`ofSheafStonean` 📖	CompOp	—

---

← Back to Index