Documentation Verification Report

LocallyConstant

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

Statistics

Metric	Count
Definitions `adjunction`, `componentHom`, `counit`, `counitApp`, `counitAppApp`, `counitAppAppImage`, `fiber`, `functor`, `functorIso`, `functorToPresheaves`, `functorToPresheavesIso`, `locallyConstantIsoContinuousMap`, `sigmaIncl`, `sigmaIso`, `unit`, `unitIso`, `functor`, `functorFullyFaithful`, `iso`, `functor`, `functorFullyFaithful`, `iso`	22
Theorems `adjunction_counit`, `adjunction_left_triangle`, `adjunction_unit`, `counitApp_app`, `counit_app_val`, `functorToPresheaves_map_app`, `functorToPresheaves_obj_map`, `functorToPresheaves_obj_obj`, `functor_map_val`, `functor_obj_val`, `incl_comap`, `incl_of_counitAppApp`, `instHasPropCarrierToTopFiber`, `instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction`, `locallyConstantIsoContinuousMap_hom`, `locallyConstantIsoContinuousMap_inv_apply`, `presheaf_ext`, `sigmaComparison_comp_sigmaIso`, `unit_app`, `instFaithfulCondensedTypeDiscrete`, `instFaithfulFunctor`, `instFullCondensedTypeDiscrete`, `instFullFunctor`, `instFaithfulFunctor`, `instFaithfulLightCondensedTypeDiscrete`, `instFullFunctor`, `instFullLightCondensedTypeDiscrete`, `instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop`	28
Total	50

CompHausLike.LocallyConstant

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	3 math math: `adjunction_counit`, `instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction`, `adjunction_unit`
`componentHom` 📖	CompOp	1 math math: `incl_comap`
`counit` 📖	CompOp	3 math math: `adjunction_counit`, `adjunction_left_triangle`, `counit_app_val`
`counitApp` 📖	CompOp	4 math math: `counitApp_app`, `LightCondensed.isoLocallyConstantOfIsColimit_inv`, `Condensed.isoLocallyConstantOfIsColimit_inv`, `counit_app_val`
`counitAppApp` 📖	CompOp	2 math math: `counitApp_app`, `incl_of_counitAppApp`
`counitAppAppImage` 📖	CompOp	1 math math: `incl_of_counitAppApp`
`fiber` 📖	CompOp	4 math math: `instHasPropCarrierToTopFiber`, `incl_of_counitAppApp`, `sigmaComparison_comp_sigmaIso`, `incl_comap`
`functor` 📖	CompOp	8 math math: `adjunction_counit`, `functor_map_val`, `functor_obj_val`, `adjunction_left_triangle`, `instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction`, `counit_app_val`, `unit_app`, `adjunction_unit`
`functorIso` 📖	CompOp	—
`functorToPresheaves` 📖	CompOp	7 math math: `counitApp_app`, `functor_map_val`, `functor_obj_val`, `functorToPresheaves_map_app`, `adjunction_left_triangle`, `functorToPresheaves_obj_map`, `functorToPresheaves_obj_obj`
`functorToPresheavesIso` 📖	CompOp	—
`locallyConstantIsoContinuousMap` 📖	CompOp	2 math math: `locallyConstantIsoContinuousMap_inv_apply`, `locallyConstantIsoContinuousMap_hom`
`sigmaIncl` 📖	CompOp	3 math math: `incl_of_counitAppApp`, `sigmaComparison_comp_sigmaIso`, `incl_comap`
`sigmaIso` 📖	CompOp	1 math math: `sigmaComparison_comp_sigmaIso`
`unit` 📖	CompOp	3 math math: `adjunction_left_triangle`, `unit_app`, `adjunction_unit`
`unitIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjunction_counit` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.Adjunction.counit` `CategoryTheory.types` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `adjunction` `counit`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`adjunction_left_triangle` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `functorToPresheaves` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.Sheaf.Hom.val` `counit` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CategoryTheory.types_ext` `presheaf_ext` `CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal` `incl_of_counitAppApp` `LocallyConstant.ext` `DiscreteTopology.toT2Space` `instDiscreteTopologyPUnit` `Function.Fiber.map_eq_image`
`adjunction_unit` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.Adjunction.unit` `CategoryTheory.types` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `adjunction` `unit`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`counitApp_app` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str`	`CategoryTheory.NatTrans.app` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorToPresheaves` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `counitApp` `counitAppApp` `Opposite.unop`	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`counit_app_val` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.coherentTopology` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.Sheaf.instCategorySheaf` `CategoryTheory.Functor.comp` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `functor` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `counit` `counitApp` `CategoryTheory.Sheaf.val`	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular`
`functorToPresheaves_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `LocallyConstant` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `LocallyConstant.comap` `Opposite.unop` `TopCat.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `TopCat` `TopCat.instCategory` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorToPresheaves` `LocallyConstant.map`	—	—
`functorToPresheaves_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorToPresheaves` `LocallyConstant.comap` `TopCat.carrier` `CompHausLike.toTop` `Opposite.unop` `TopCat.str` `TopCat.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `TopCat` `TopCat.instCategory` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`functorToPresheaves_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorToPresheaves` `LocallyConstant` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	—
`functor_map_val` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.Sheaf.Hom.val` `CategoryTheory.coherentTopology` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `functorToPresheaves` `CategoryTheory.Functor.map` `CategoryTheory.Sheaf` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular`
`functor_obj_val` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `functorToPresheaves`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular`
`incl_comap` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str`	`CategoryTheory.CategoryStruct.comp` `Opposite` `CompHausLike` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `Opposite.op` `fiber` `Opposite.unop` `CategoryTheory.Functor.obj` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `LocallyConstant.comap` `TopCat.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `TopCat` `TopCat.instCategory` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `Quiver.Hom.op` `sigmaIncl` `DFunLike.coe` `LocallyConstant` `LocallyConstant.instFunLike` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `Function.Fiber.preimage` `componentHom`	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`incl_of_counitAppApp` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str`	`CategoryTheory.Functor.map` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `Opposite.op` `fiber` `CategoryTheory.Functor.obj` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `sigmaIncl` `counitAppApp` `counitAppAppImage`	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant` `CompHausLike.is_compact` `CompHausLike.HasExplicitFiniteCoproducts.hasProp` `CompHausLike.is_hausdorff` `instHasPropCarrierToTopFiber` `sigmaComparison_comp_sigmaIso` `CategoryTheory.Functor.mapIso_hom` `CategoryTheory.Iso.op_hom` `CategoryTheory.types_comp_apply` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.FunctorToTypes.map_id_apply` `instCompactSpaceSigmaOfFinite` `Sigma.t2Space` `CompHausLike.instHasPropSigma` `CompHausLike.isIsoSigmaComparison` `CategoryTheory.inv_hom_id_apply`
`instHasPropCarrierToTopFiber` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str`	`fiber`	—	—
`instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `CategoryTheory.Adjunction.unit` `adjunction`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CategoryTheory.Iso.isIso_hom`
`locallyConstantIsoContinuousMap_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.types` `LocallyConstant` `ContinuousMap` `TopCat.carrier` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `TopCat.discrete` `TopCat.str` `locallyConstantIsoContinuousMap` `LocallyConstant.toContinuousMap` `Bot.bot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`locallyConstantIsoContinuousMap_inv_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `LocallyConstant.instFunLike` `CategoryTheory.Iso.inv` `CategoryTheory.types` `ContinuousMap` `TopCat.carrier` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `TopCat.discrete` `TopCat.str` `locallyConstantIsoContinuousMap` `ContinuousMap.instFunLike`	—	—
`presheaf_ext` 📖	—	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str` `CategoryTheory.Functor.map` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `Opposite.op` `fiber` `CategoryTheory.Functor.obj` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `sigmaIncl`	—	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CategoryTheory.injective_of_mono` `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant` `CompHausLike.is_compact` `CompHausLike.HasExplicitFiniteCoproducts.hasProp` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `instCompactSpaceSigmaOfFinite` `Sigma.t2Space` `CompHausLike.is_hausdorff` `CompHausLike.instHasPropSigma` `instHasPropCarrierToTopFiber` `CompHausLike.isIsoSigmaComparison` `sigmaComparison_comp_sigmaIso`
`sigmaComparison_comp_sigmaIso` 📖	mathematical	`CompHausLike.HasProp` `TopCat.carrier` `CompHausLike.toTop` `instTopologicalSpaceSubtype` `TopCat.str`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.Functor.obj` `Opposite` `CompHausLike` `CategoryTheory.Category.opposite` `CompHausLike.category` `Opposite.op` `CompHausLike.finiteCoproduct` `Function.Fiber` `DFunLike.coe` `LocallyConstant` `LocallyConstant.instFunLike` `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant` `CompHausLike.is_compact` `fiber` `CompHausLike.HasExplicitFiniteCoproducts.hasProp` `CompHausLike.of` `CompHausLike.is_hausdorff` `instHasPropCarrierToTopFiber` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.mapIso` `CategoryTheory.Iso.op` `sigmaIso` `CompHausLike.sigmaComparison` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `sigmaIncl`	—	`CategoryTheory.types_ext` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `instHasPropCarrierToTopFiber` `TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant` `CompHausLike.HasExplicitFiniteCoproducts.hasProp` `instCompactSpaceSigmaOfFinite` `Sigma.t2Space` `CompHausLike.instHasPropSigma` `continuous_sigmaMk`
`unit_app` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.NatTrans.app` `CategoryTheory.types` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Sheaf` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `CategoryTheory.Sheaf.instCategorySheaf` `functor` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.sheafSections` `Opposite.op` `CompHausLike.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `unit` `LocallyConstant.const`	—	`CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHausLike.preregular` `Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`

CondensedSet.LocallyConstant

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	4 math math: `CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone`, `instFaithfulFunctor`, `CondensedSet.isDiscrete_tfae`, `instFullFunctor`
`functorFullyFaithful` 📖	CompOp	—
`iso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulCondensedTypeDiscrete` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `Condensed` `instCategoryCondensed` `Condensed.discrete` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CompHaus` `CompHausLike.category` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget`	—	`CategoryTheory.Functor.Faithful.of_iso` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget` `instFaithfulFunctor`
`instFaithfulFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `CondensedSet` `instCategoryCondensed` `functor`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFullCondensedTypeDiscrete` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.types` `Condensed` `instCategoryCondensed` `Condensed.discrete` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CompHaus` `CompHausLike.category` `CategoryTheory.coherentTopology` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget`	—	`CategoryTheory.Functor.Full.of_iso` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHaus.instPreregular` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.reflectsIsomorphisms_of_full_and_faithful` `CategoryTheory.Types.instFullForgetTypeHom` `CategoryTheory.instFaithfulForget` `instFullFunctor`
`instFullFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.types` `CondensedSet` `instCategoryCondensed` `functor`	—	`CategoryTheory.Functor.FullyFaithful.full`

LightCondSet.LocallyConstant

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	4 math math: `instFaithfulFunctor`, `LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone`, `instFullFunctor`, `LightCondSet.isDiscrete_tfae`
`functorFullyFaithful` 📖	CompOp	—
`iso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `LightCondSet` `instCategoryLightCondensed` `functor`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFaithfulLightCondensedTypeDiscrete` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.types` `LightCondensed` `instCategoryLightCondensed` `LightCondensed.discrete` `LightProfinite.hasSheafify_type`	—	`CategoryTheory.Functor.Faithful.of_iso` `LightProfinite.hasSheafify_type` `instFaithfulFunctor`
`instFullFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.types` `LightCondSet` `instCategoryLightCondensed` `functor`	—	`CategoryTheory.Functor.FullyFaithful.full`
`instFullLightCondensedTypeDiscrete` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CategoryTheory.types` `LightCondensed` `instCategoryLightCondensed` `LightCondensed.discrete` `LightProfinite.hasSheafify_type`	—	`CategoryTheory.Functor.Full.of_iso` `LightProfinite.hasSheafify_type` `instFullFunctor`
`instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop` 📖	mathematical	—	`CompHausLike.HasProp` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CompHausLike.toTop` `instTopologicalSpaceSubtype`	—	`Subtype.totallyDisconnectedSpace` `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology` `LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace`

---

← Back to Index