FinTopCat

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

Statistics

Metric	Count
Definitions FinTopCat, fintype, instCategory, instCoeSortType, instConcreteCategoryContinuousMapCarrierToTop, instFintypeCarrierObjTopCatForget₂ContinuousMapToTop, instHasForget₂ContinuousMapCarrierToTopFintypeCatHomObjFinite, instHasForget₂ContinuousMapCarrierToTopTopCat, instInhabited, instTopologicalSpaceObjFiniteObjFintypeCatForget₂ContinuousMapCarrierToTopHom, of, toTop, instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier, instTopologicalSpaceObjFinite	14
Theorems coe_of, instDiscreteTopologyObjFinite	2
Total	16

FinTopCat

Definitions

Name	Category	Theorems
fintype 📖	CompOp	—
instCategory 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instConcreteCategoryContinuousMapCarrierToTop 📖	CompOp	—
instFintypeCarrierObjTopCatForget₂ContinuousMapToTop 📖	CompOp	—
instHasForget₂ContinuousMapCarrierToTopFintypeCatHomObjFinite 📖	CompOp	—
instHasForget₂ContinuousMapCarrierToTopTopCat 📖	CompOp	—
instInhabited 📖	CompOp	—
instTopologicalSpaceObjFiniteObjFintypeCatForget₂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₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier 📖	CompOp	7 math math: CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.PreGaloisCategory.functorToContAction_map, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction
instTopologicalSpaceObjFinite 📖	CompOp	1 math math: instDiscreteTopologyObjFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopologyObjFinite 📖	mathematical	—	DiscreteTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite instTopologicalSpaceObjFinite	—	—

(root)

Definitions

Name	Category	Theorems
FinTopCat 📖	CompData	—

---

← Back to Index