OfSection

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

Statistics

Metric	Count
Definitions ofSection, ofSection	2
Theorems mem_ofSection_obj, ofSection_eq_range, ofSection_eq_range', ofSection_image, ofSection_le_iff, range_eq_ofSection, range_eq_ofSection', mem_ofSection_obj, ofSection_eq_range, ofSection_eq_range', ofSection_image, ofSection_le_iff, ofSection_obj, range_eq_ofSection, range_eq_ofSection'	15
Total	17

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
ofSection 📖	CompOp	21 math math: Subpresheaf.range_eq_ofSection', Subpresheaf.range_eq_ofSection, ofSection_eq_range, Subpresheaf.ofSection_eq_range', isGeneratedBy_iff, Subpresheaf.isGeneratedBy_iff, IsGeneratedBy.ofSection_le, ofSection_obj, Subpresheaf.mem_ofSection_obj, ofSection_eq_range', range_eq_ofSection', IsGeneratedBy.iSup_eq, range_eq_ofSection, mem_ofSection_obj, ofSection_image, ofSection_le_iff, Subpresheaf.ofSection_le_iff, Subpresheaf.ofSection_image, Subpresheaf.IsGeneratedBy.ofSection_le, Subpresheaf.ofSection_eq_range, Subpresheaf.IsGeneratedBy.iSup_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ofSection_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Set Set.instMembership obj ofSection	—	CategoryTheory.FunctorToTypes.map_id_apply
ofSection_eq_range 📖	mathematical	—	ofSection range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv	—	ext Set.ext
ofSection_eq_range' 📖	mathematical	—	ofSection range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	ext Set.ext
ofSection_image 📖	mathematical	—	image Opposite CategoryTheory.Category.opposite ofSection CategoryTheory.NatTrans.app CategoryTheory.types	—	le_antisymm image_le_iff ofSection_le_iff preimage_obj Set.mem_preimage CategoryTheory.FunctorToTypes.map_id_apply mem_ofSection_obj
ofSection_le_iff 📖	mathematical	—	CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor ofSection CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership obj	—	mem_ofSection_obj map
ofSection_obj 📖	mathematical	—	obj Opposite CategoryTheory.Category.opposite ofSection setOf CategoryTheory.Functor.obj CategoryTheory.types Quiver.Hom Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	—	—
range_eq_ofSection 📖	mathematical	—	range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda ofSection Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv	—	ofSection_eq_range Equiv.symm_apply_apply
range_eq_ofSection' 📖	mathematical	—	range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.uliftFunctor ofSection Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.uliftYoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv	—	ofSection_eq_range' Equiv.symm_apply_apply

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
ofSection 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ofSection_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj CategoryTheory.Subfunctor.ofSection	—	CategoryTheory.Subfunctor.mem_ofSection_obj
ofSection_eq_range 📖	mathematical	—	CategoryTheory.Subfunctor.ofSection CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv	—	CategoryTheory.Subfunctor.ofSection_eq_range
ofSection_eq_range' 📖	mathematical	—	CategoryTheory.Subfunctor.ofSection CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.uliftYoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Subfunctor.ofSection_eq_range'
ofSection_image 📖	mathematical	—	CategoryTheory.Subfunctor.image Opposite CategoryTheory.Category.opposite CategoryTheory.Subfunctor.ofSection CategoryTheory.NatTrans.app CategoryTheory.types	—	CategoryTheory.Subfunctor.ofSection_image
ofSection_le_iff 📖	mathematical	—	CategoryTheory.Subfunctor Opposite CategoryTheory.Category.opposite Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Subfunctor.ofSection CategoryTheory.Functor.obj CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Subfunctor.ofSection_le_iff
range_eq_ofSection 📖	mathematical	—	CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Subfunctor.ofSection Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv	—	CategoryTheory.Subfunctor.range_eq_ofSection
range_eq_ofSection' 📖	mathematical	—	CategoryTheory.Subfunctor.range Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.uliftFunctor CategoryTheory.Subfunctor.ofSection Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.uliftYoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.uliftYonedaEquiv	—	CategoryTheory.Subfunctor.range_eq_ofSection'

---

← Back to Index