Documentation Verification Report

Basic

📁 Source: Mathlib/Condensed/Discrete/Basic.lean

Statistics

Metric	Count
Definitions `discrete`, `discreteUnderlyingAdj`, `underlying`, `discrete`, `discreteUnderlyingAdj`, `underlying`, `discrete`, `discreteUnderlyingAdj`, `underlying`	9
Theorems `discrete_map`, `discrete_obj`, `underlying_map`, `underlying_obj`, `discrete_map`, `discrete_obj`, `underlying_map`, `underlying_obj`	8
Total	17

Condensed

Definitions

Name	Category	Theorems
`discrete` 📖	CompOp	9 math math: `CondensedMod.isDiscrete_tfae`, `discrete_map`, `CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete`, `CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete`, `CondensedSet.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete`, `CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete`, `discrete_obj`
`discreteUnderlyingAdj` 📖	CompOp	3 math math: `CondensedMod.isDiscrete_tfae`, `CondensedSet.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`
`underlying` 📖	CompOp	5 math math: `CondensedMod.isDiscrete_tfae`, `CondensedSet.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `underlying_obj`, `underlying_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discrete_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Condensed` `instCategoryCondensed` `discrete` `CategoryTheory.Functor` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular`
`discrete_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Condensed` `instCategoryCondensed` `discrete` `CategoryTheory.Functor` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.const`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular`
`underlying_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Condensed` `instCategoryCondensed` `underlying` `CategoryTheory.NatTrans.app` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.Hom.val` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit`	—	—
`underlying_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Condensed` `instCategoryCondensed` `underlying` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit`	—	—

LightCondSet

Definitions

Name	Category	Theorems
`discrete` 📖	CompOp	—
`discreteUnderlyingAdj` 📖	CompOp	—
`underlying` 📖	CompOp	—

LightCondensed

Definitions

Name	Category	Theorems
`discrete` 📖	CompOp	9 math math: `LightCondMod.isDiscrete_tfae`, `discrete_map`, `LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete`, `LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete`, `LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete`, `discrete_obj`, `LightCondSet.isDiscrete_tfae`, `LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete`
`discreteUnderlyingAdj` 📖	CompOp	3 math math: `LightCondMod.isDiscrete_tfae`, `LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `LightCondSet.isDiscrete_tfae`
`underlying` 📖	CompOp	5 math math: `LightCondMod.isDiscrete_tfae`, `LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `underlying_obj`, `LightCondSet.isDiscrete_tfae`, `underlying_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`discrete_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `LightCondensed` `instCategoryLightCondensed` `discrete` `CategoryTheory.Functor` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular`
`discrete_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `LightCondensed` `instCategoryLightCondensed` `discrete` `CategoryTheory.Functor` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Functor.category` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.presheafToSheaf` `CategoryTheory.Functor.const`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `LightProfinite.instPreregular`
`underlying_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `LightCondensed` `instCategoryLightCondensed` `underlying` `CategoryTheory.NatTrans.app` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.Sheaf.Hom.val` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit`	—	—
`underlying_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `LightCondensed` `instCategoryLightCondensed` `underlying` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit`	—	—

---

← Back to Index