Documentation Verification Report

FinTopCat

📁 Source: Mathlib/Topology/Category/FinTopCat.lean

Statistics

Metric	Count
Definitions `FinTopCat`, `fintype`, `instCategory`, `instCoeSortType`, `instConcreteCategoryContinuousMapCarrierToTop`, `instFintypeCarrierObjTopCatForget₂ContinuousMapToTop`, `instHasForget₂ContinuousMapCarrierToTopFintypeCatHomCarrier`, `instHasForget₂ContinuousMapCarrierToTopTopCat`, `instInhabited`, `instTopologicalSpaceCarrierObjFintypeCatForget₂ContinuousMapCarrierToTopHom`, `of`, `toTop`, `instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier`, `instTopologicalSpaceCarrier`	14
Theorems `coe_of`, `instDiscreteTopologyCarrier`	2
Total	16

FinTopCat

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	—
`instCategory` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryContinuousMapCarrierToTop` 📖	CompOp	—
`instFintypeCarrierObjTopCatForget₂ContinuousMapToTop` 📖	CompOp	—
`instHasForget₂ContinuousMapCarrierToTopFintypeCatHomCarrier` 📖	CompOp	—
`instHasForget₂ContinuousMapCarrierToTopTopCat` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instTopologicalSpaceCarrierObjFintypeCatForget₂ContinuousMapCarrierToTopHom` 📖	CompOp	—
`of` 📖	CompOp	1 math math: `coe_of`
`toTop` 📖	CompOp	1 math math: `coe_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`TopCat.carrier` `toTop` `of`	—	—

FintypeCatDiscrete

Definitions

Name	Category	Theorems
`instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier` 📖	CompOp	7 math math: `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.functorToContAction_map`, `CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor`, `CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj`
`instTopologicalSpaceCarrier` 📖	CompOp	1 math math: `instDiscreteTopologyCarrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instDiscreteTopologyCarrier` 📖	mathematical	—	`DiscreteTopology` `FintypeCat.carrier` `instTopologicalSpaceCarrier`	—	—

(root)

Definitions

Name	Category	Theorems
`FinTopCat` 📖	CompData	—

---

← Back to Index