Finite

📁 Source: Mathlib/CategoryTheory/Subfunctor/Finite.lean

Statistics

Metric	Count
Definitions PresheafIsFinite, PresheafIsGeneratedBy, X, x, IsGeneratedBy, X, x, IsGeneratedBy	8
Theorems of_epi, range, exists_isGeneratedBy, instFiniteIndex, iSup_eq, image, isFinite, mem, ofSection_le, of_equiv, iSup_eq, image, isFinite, mem, ofSection_le, of_equiv, image_isFinite, isGeneratedBy_iff, isGeneratedBy_of_isFinite, image_isFinite, isGeneratedBy_iff, isGeneratedBy_of_isFinite, range_isFinite, instPresheafIsFiniteObjFunctorOppositeTypeYoneda, presheafIsFinite_of_epi, presheafIsGeneratedBy_of_isFinite, yoneda_obj_isGeneratedBy	27
Total	35

CategoryTheory

Definitions

Name	Category	Theorems
PresheafIsFinite 📖	MathDef	2 math math: presheafIsFinite_of_epi, instPresheafIsFiniteObjFunctorOppositeTypeYoneda
PresheafIsGeneratedBy 📖	MathDef	2 math math: presheafIsGeneratedBy_of_isFinite, yoneda_obj_isGeneratedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPresheafIsFiniteObjFunctorOppositeTypeYoneda 📖	mathematical	—	PresheafIsFinite Functor.obj Functor Opposite Category.opposite types Functor.category yoneda	—	Subfunctor.IsGeneratedBy.isFinite Finite.of_fintype yoneda_obj_isGeneratedBy
presheafIsFinite_of_epi 📖	mathematical	—	PresheafIsFinite	—	Subfunctor.IsGeneratedBy.isFinite Subfunctor.IsFinite.instFiniteIndex PresheafIsGeneratedBy.of_epi presheafIsGeneratedBy_of_isFinite
presheafIsGeneratedBy_of_isFinite 📖	mathematical	—	PresheafIsGeneratedBy Subfunctor.IsFinite.Index Top.top Subfunctor Opposite Category.opposite OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticeSubfunctor BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Subfunctor.IsFinite.X Subfunctor.IsFinite.x	—	Subfunctor.isGeneratedBy_of_isFinite
yoneda_obj_isGeneratedBy 📖	mathematical	—	PresheafIsGeneratedBy Functor.obj Functor Opposite Category.opposite types Functor.category yoneda Opposite.op CategoryStruct.id Category.toCategoryStruct	—	Subfunctor.ext Set.ext Subfunctor.iSup_obj Category.comp_id

CategoryTheory.PresheafIsGeneratedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_epi 📖	mathematical	CategoryTheory.PresheafIsGeneratedBy	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	CategoryTheory.Subfunctor.range_eq_top range
range 📖	mathematical	CategoryTheory.PresheafIsGeneratedBy	CategoryTheory.Subfunctor.IsGeneratedBy CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite CategoryTheory.NatTrans.app CategoryTheory.types	—	CategoryTheory.Subfunctor.IsGeneratedBy.image

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
IsGeneratedBy 📖	MathDef	6 math math: Subpresheaf.isGeneratedBy_of_isFinite, isGeneratedBy_of_isFinite, isGeneratedBy_iff, Subpresheaf.isGeneratedBy_iff, IsFinite.exists_isGeneratedBy, CategoryTheory.PresheafIsGeneratedBy.range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_isFinite 📖	mathematical	—	IsFinite image Opposite CategoryTheory.Category.opposite	—	IsGeneratedBy.isFinite IsFinite.instFiniteIndex IsGeneratedBy.image isGeneratedBy_of_isFinite
isGeneratedBy_iff 📖	mathematical	—	IsGeneratedBy iSup CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor ofSection	—	—
isGeneratedBy_of_isFinite 📖	mathematical	—	IsGeneratedBy IsFinite.Index IsFinite.X IsFinite.x	—	IsFinite.exists_isGeneratedBy
range_isFinite 📖	mathematical	—	IsFinite range Opposite CategoryTheory.Category.opposite	—	IsGeneratedBy.isFinite IsFinite.instFiniteIndex CategoryTheory.PresheafIsGeneratedBy.range CategoryTheory.presheafIsGeneratedBy_of_isFinite

CategoryTheory.Subfunctor.IsFinite

Definitions

Name	Category	Theorems
X 📖	CompOp	3 math math: CategoryTheory.Subfunctor.Subpresheaf.isGeneratedBy_of_isFinite, CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite, CategoryTheory.presheafIsGeneratedBy_of_isFinite
x 📖	CompOp	3 math math: CategoryTheory.Subfunctor.Subpresheaf.isGeneratedBy_of_isFinite, CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite, CategoryTheory.presheafIsGeneratedBy_of_isFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isGeneratedBy 📖	mathematical	—	CategoryTheory.Subfunctor.IsGeneratedBy	—	—
instFiniteIndex 📖	mathematical	—	Finite Index	—	exists_isGeneratedBy

CategoryTheory.Subfunctor.IsGeneratedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_eq 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	iSup CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor CategoryTheory.Subfunctor.ofSection	—	—
image 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor.image Opposite CategoryTheory.Category.opposite CategoryTheory.NatTrans.app CategoryTheory.types	—	iSup_eq CategoryTheory.Subfunctor.image_iSup CategoryTheory.Subfunctor.ofSection_image
isFinite 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor.IsFinite	—	Finite.exists_equiv_fin Finite.of_fintype of_equiv
mem 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.ofSection_le_iff ofSection_le
ofSection_le 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Subfunctor.ofSection	—	iSup_eq le_iSup
of_equiv 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	CategoryTheory.Subfunctor.isGeneratedBy_iff iSup_eq Equiv.iSup_congr

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
IsGeneratedBy 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_isFinite 📖	mathematical	—	CategoryTheory.Subfunctor.IsFinite CategoryTheory.Subfunctor.image Opposite CategoryTheory.Category.opposite	—	CategoryTheory.Subfunctor.image_isFinite
isGeneratedBy_iff 📖	mathematical	—	CategoryTheory.Subfunctor.IsGeneratedBy iSup CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor CategoryTheory.Subfunctor.ofSection	—	CategoryTheory.Subfunctor.isGeneratedBy_iff
isGeneratedBy_of_isFinite 📖	mathematical	—	CategoryTheory.Subfunctor.IsGeneratedBy CategoryTheory.Subfunctor.IsFinite.Index CategoryTheory.Subfunctor.IsFinite.X CategoryTheory.Subfunctor.IsFinite.x	—	CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite

CategoryTheory.Subfunctor.Subpresheaf.IsFinite

Definitions

Name	Category	Theorems
X 📖	CompOp	—
x 📖	CompOp	—

CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_eq 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	iSup CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup CategoryTheory.instCompleteLatticeSubfunctor CategoryTheory.Subfunctor.ofSection	—	CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq
image 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor.image Opposite CategoryTheory.Category.opposite CategoryTheory.NatTrans.app CategoryTheory.types	—	CategoryTheory.Subfunctor.IsGeneratedBy.image
isFinite 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor.IsFinite	—	CategoryTheory.Subfunctor.IsGeneratedBy.isFinite
mem 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.IsGeneratedBy.mem
ofSection_le 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Subfunctor.ofSection	—	CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le
of_equiv 📖	mathematical	CategoryTheory.Subfunctor.IsGeneratedBy	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv

---

← Back to Index