Opposites

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean

Statistics

Metric	Count
Definitions	0
Theorems preservesColimit_leftOp, preservesColimit_of_leftOp, preservesColimit_of_op, preservesColimit_of_rightOp, preservesColimit_of_unop, preservesColimit_op, preservesColimit_rightOp, preservesColimit_unop, preservesColimitsOfShape_leftOp, preservesColimitsOfShape_of_leftOp, preservesColimitsOfShape_of_op, preservesColimitsOfShape_of_rightOp, preservesColimitsOfShape_of_unop, preservesColimitsOfShape_op, preservesColimitsOfShape_rightOp, preservesColimitsOfShape_unop, preservesColimitsOfSize_leftOp, preservesColimitsOfSize_of_leftOp, preservesColimitsOfSize_of_op, preservesColimitsOfSize_of_rightOp, preservesColimitsOfSize_of_unop, preservesColimitsOfSize_op, preservesColimitsOfSize_rightOp, preservesColimitsOfSize_unop, preservesColimits_leftOp, preservesColimits_of_leftOp, preservesColimits_of_op, preservesColimits_of_rightOp, preservesColimits_of_unop, preservesColimits_op, preservesColimits_rightOp, preservesColimits_unop, preservesFiniteColimits_leftOp, preservesFiniteColimits_of_leftOp, preservesFiniteColimits_of_op, preservesFiniteColimits_of_rightOp, preservesFiniteColimits_of_unop, preservesFiniteColimits_op, preservesFiniteColimits_rightOp, preservesFiniteColimits_unop, preservesFiniteCoproducts_leftOp, preservesFiniteCoproducts_op, preservesFiniteCoproducts_rightOp, preservesFiniteCoproducts_unop, preservesFiniteLimits_leftOp, preservesFiniteLimits_of_leftOp, preservesFiniteLimits_of_op, preservesFiniteLimits_of_rightOp, preservesFiniteLimits_of_unop, preservesFiniteLimits_op, preservesFiniteLimits_rightOp, preservesFiniteLimits_unop, preservesFiniteProducts_leftOp, preservesFiniteProducts_op, preservesFiniteProducts_rightOp, preservesFiniteProducts_unop, preservesLimit_leftOp, preservesLimit_of_leftOp, preservesLimit_of_op, preservesLimit_of_rightOp, preservesLimit_of_unop, preservesLimit_op, preservesLimit_rightOp, preservesLimit_unop, preservesLimitsOfShape_leftOp, preservesLimitsOfShape_of_leftOp, preservesLimitsOfShape_of_op, preservesLimitsOfShape_of_rightOp, preservesLimitsOfShape_of_unop, preservesLimitsOfShape_op, preservesLimitsOfShape_rightOp, preservesLimitsOfShape_unop, preservesLimitsOfSize_leftOp, preservesLimitsOfSize_of_leftOp, preservesLimitsOfSize_of_op, preservesLimitsOfSize_of_rightOp, preservesLimitsOfSize_of_unop, preservesLimitsOfSize_op, preservesLimitsOfSize_rightOp, preservesLimitsOfSize_unop, preservesLimits_leftOp, preservesLimits_of_leftOp, preservesLimits_of_op, preservesLimits_of_rightOp, preservesLimits_of_unop, preservesLimits_op, preservesLimits_rightOp, preservesLimits_unop, reflectsColimit_leftOp, reflectsColimit_of_leftOp, reflectsColimit_of_op, reflectsColimit_of_rightOp, reflectsColimit_of_unop, reflectsColimit_op, reflectsColimit_rightOp, reflectsColimit_unop, reflectsColimitsOfShape_leftOp, reflectsColimitsOfShape_of_leftOp, reflectsColimitsOfShape_of_op, reflectsColimitsOfShape_of_rightOp, reflectsColimitsOfShape_of_unop, reflectsColimitsOfShape_op, reflectsColimitsOfShape_rightOp, reflectsColimitsOfShape_unop, reflectsColimitsOfSize_leftOp, reflectsColimitsOfSize_of_leftOp, reflectsColimitsOfSize_of_op, reflectsColimitsOfSize_of_rightOp, reflectsColimitsOfSize_of_unop, reflectsColimitsOfSize_op, reflectsColimitsOfSize_rightOp, reflectsColimitsOfSize_unop, reflectsColimits_leftOp, reflectsColimits_of_leftOp, reflectsColimits_of_op, reflectsColimits_of_rightOp, reflectsColimits_of_unop, reflectsColimits_op, reflectsColimits_rightOp, reflectsColimits_unop, reflectsFiniteColimits_leftOp, reflectsFiniteColimits_of_leftOp, reflectsFiniteColimits_of_op, reflectsFiniteColimits_of_rightOp, reflectsFiniteColimits_of_unop, reflectsFiniteColimits_op, reflectsFiniteColimits_rightOp, reflectsFiniteColimits_unop, reflectsFiniteCoproducts_leftOp, reflectsFiniteCoproducts_op, reflectsFiniteCoproducts_rightOp, reflectsFiniteCoproducts_unop, reflectsFiniteLimits_leftOp, reflectsFiniteLimits_of_leftOp, reflectsFiniteLimits_of_op, reflectsFiniteLimits_of_rightOp, reflectsFiniteLimits_of_unop, reflectsFiniteLimits_op, reflectsFiniteLimits_rightOp, reflectsFiniteLimits_unop, reflectsFiniteProducts_leftOp, reflectsFiniteProducts_op, reflectsFiniteProducts_rightOp, reflectsFiniteProducts_unop, reflectsLimit_leftOp, reflectsLimit_of_leftOp, reflectsLimit_of_op, reflectsLimit_of_rightOp, reflectsLimit_of_unop, reflectsLimit_op, reflectsLimit_rightOp, reflectsLimit_unop, reflectsLimitsOfShape_leftOp, reflectsLimitsOfShape_of_leftOp, reflectsLimitsOfShape_of_op, reflectsLimitsOfShape_of_rightOp, reflectsLimitsOfShape_of_unop, reflectsLimitsOfShape_op, reflectsLimitsOfShape_rightOp, reflectsLimitsOfShape_unop, reflectsLimitsOfSize_leftOp, reflectsLimitsOfSize_of_leftOp, reflectsLimitsOfSize_of_op, reflectsLimitsOfSize_of_rightOp, reflectsLimitsOfSize_of_unop, reflectsLimitsOfSize_op, reflectsLimitsOfSize_rightOp, reflectsLimitsOfSize_unop, reflectsLimits_leftOp, reflectsLimits_of_leftOp, reflectsLimits_of_op, reflectsLimits_of_rightOp, reflectsLimits_of_unop, reflectsLimits_op, reflectsLimits_rightOp, reflectsLimits_unop	176
Total	176

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesColimit_leftOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
preservesColimit_of_leftOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_of_op 📖	mathematical	—	PreservesColimit	—	—
preservesColimit_of_rightOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_of_unop 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite	—	—
preservesColimit_op 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
preservesColimit_rightOp 📖	mathematical	—	PreservesColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
preservesColimit_unop 📖	mathematical	—	PreservesColimit CategoryTheory.Functor.unop	—	—
preservesColimitsOfShape_leftOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimit_leftOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_leftOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_leftOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_op 📖	mathematical	—	PreservesColimitsOfShape	—	preservesColimit_of_op PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_rightOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_rightOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_of_unop 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesColimit_of_unop PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_op 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimit_op PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_rightOp 📖	mathematical	—	PreservesColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimit_rightOp PreservesLimitsOfShape.preservesLimit
preservesColimitsOfShape_unop 📖	mathematical	—	PreservesColimitsOfShape CategoryTheory.Functor.unop	—	preservesColimit_unop PreservesLimitsOfShape.preservesLimit
preservesColimitsOfSize_leftOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_leftOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_op 📖	mathematical	—	PreservesColimitsOfSize	—	preservesColimitsOfShape_of_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_rightOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_of_unop 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_op 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_rightOp 📖	mathematical	—	PreservesColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimitsOfSize_unop 📖	mathematical	—	PreservesColimitsOfSize CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_leftOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_leftOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_op 📖	mathematical	—	PreservesColimits	—	preservesColimitsOfShape_of_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_rightOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_of_unop 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_op 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_rightOp 📖	mathematical	—	PreservesColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesLimitsOfSize.preservesLimitsOfShape
preservesColimits_unop 📖	mathematical	—	PreservesColimits CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesLimitsOfSize.preservesLimitsOfShape
preservesFiniteColimits_leftOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_leftOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_leftOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_op 📖	mathematical	—	PreservesFiniteColimits	—	preservesColimitsOfShape_of_op PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_rightOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_rightOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_of_unop 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite	—	preservesColimitsOfShape_of_unop PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_op 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_rightOp 📖	mathematical	—	PreservesFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteColimits_unop 📖	mathematical	—	PreservesFiniteColimits CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop PreservesFiniteLimits.preservesFiniteLimits
preservesFiniteCoproducts_leftOp 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesColimitsOfShape_leftOp preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_op 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesColimitsOfShape_op preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_rightOp 📖	mathematical	—	PreservesFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesColimitsOfShape_rightOp preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteCoproducts_unop 📖	mathematical	—	PreservesFiniteCoproducts CategoryTheory.Functor.unop	—	preservesColimitsOfShape_unop preservesLimitsOfShape_of_equiv instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype
preservesFiniteLimits_leftOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_leftOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_op 📖	mathematical	—	PreservesFiniteLimits	—	preservesLimitsOfShape_of_op PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_rightOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_of_unop 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_op 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_rightOp 📖	mathematical	—	PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteLimits_unop 📖	mathematical	—	PreservesFiniteLimits CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesFiniteColimits.preservesFiniteColimits
preservesFiniteProducts_leftOp 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_op 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_rightOp 📖	mathematical	—	PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesFiniteProducts_unop 📖	mathematical	—	PreservesFiniteProducts CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop preservesColimitsOfShape_of_equiv instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Finite.of_fintype
preservesLimit_leftOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
preservesLimit_of_leftOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_of_op 📖	mathematical	—	PreservesLimit	—	—
preservesLimit_of_rightOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_of_unop 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite	—	—
preservesLimit_op 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
preservesLimit_rightOp 📖	mathematical	—	PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
preservesLimit_unop 📖	mathematical	—	PreservesLimit CategoryTheory.Functor.unop	—	—
preservesLimitsOfShape_leftOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimit_leftOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_leftOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_leftOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_op 📖	mathematical	—	PreservesLimitsOfShape	—	preservesLimit_of_op PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_rightOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_rightOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_of_unop 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite	—	preservesLimit_of_unop PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_op 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimit_op PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_rightOp 📖	mathematical	—	PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimit_rightOp PreservesColimitsOfShape.preservesColimit
preservesLimitsOfShape_unop 📖	mathematical	—	PreservesLimitsOfShape CategoryTheory.Functor.unop	—	preservesLimit_unop PreservesColimitsOfShape.preservesColimit
preservesLimitsOfSize_leftOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_leftOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_op 📖	mathematical	—	PreservesLimitsOfSize	—	preservesLimitsOfShape_of_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_rightOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_of_unop 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_op 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_rightOp 📖	mathematical	—	PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimitsOfSize_unop 📖	mathematical	—	PreservesLimitsOfSize CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_leftOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	preservesLimitsOfShape_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_leftOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_leftOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_op 📖	mathematical	—	PreservesLimits	—	preservesLimitsOfShape_of_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_rightOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_of_unop 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite	—	preservesLimitsOfShape_of_unop PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_op 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	preservesLimitsOfShape_op PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_rightOp 📖	mathematical	—	PreservesLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	preservesLimitsOfShape_rightOp PreservesColimitsOfSize.preservesColimitsOfShape
preservesLimits_unop 📖	mathematical	—	PreservesLimits CategoryTheory.Functor.unop	—	preservesLimitsOfShape_unop PreservesColimitsOfSize.preservesColimitsOfShape
reflectsColimit_leftOp 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
reflectsColimit_of_leftOp 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite	—	—
reflectsColimit_of_op 📖	mathematical	—	ReflectsColimit	—	—
reflectsColimit_of_rightOp 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite	—	—
reflectsColimit_of_unop 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite	—	—
reflectsColimit_op 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
reflectsColimit_rightOp 📖	mathematical	—	ReflectsColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
reflectsColimit_unop 📖	mathematical	—	ReflectsColimit CategoryTheory.Functor.unop	—	—
reflectsColimitsOfShape_leftOp 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsColimit_leftOp reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_of_leftOp 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsColimit_of_leftOp reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_of_op 📖	mathematical	—	ReflectsColimitsOfShape	—	reflectsColimit_of_op reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_of_rightOp 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsColimit_of_rightOp reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_of_unop 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsColimit_of_unop reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_op 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsColimit_op reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_rightOp 📖	mathematical	—	ReflectsColimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsColimit_rightOp reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfShape_unop 📖	mathematical	—	ReflectsColimitsOfShape CategoryTheory.Functor.unop	—	reflectsColimit_unop reflectsLimit_of_reflectsLimitsOfShape
reflectsColimitsOfSize_leftOp 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsColimitsOfShape_leftOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_of_leftOp 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_leftOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_of_op 📖	mathematical	—	ReflectsColimitsOfSize	—	reflectsColimitsOfShape_of_op reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_of_rightOp 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_rightOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_of_unop 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_unop reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_op 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsColimitsOfShape_op reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_rightOp 📖	mathematical	—	ReflectsColimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsColimitsOfShape_rightOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimitsOfSize_unop 📖	mathematical	—	ReflectsColimitsOfSize CategoryTheory.Functor.unop	—	reflectsColimitsOfShape_unop reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_leftOp 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsColimitsOfShape_leftOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_of_leftOp 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_leftOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_of_op 📖	mathematical	—	ReflectsColimits	—	reflectsColimitsOfShape_of_op reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_of_rightOp 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_rightOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_of_unop 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_unop reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_op 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsColimitsOfShape_op reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_rightOp 📖	mathematical	—	ReflectsColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsColimitsOfShape_rightOp reflectsLimitsOfShape_of_reflectsLimits
reflectsColimits_unop 📖	mathematical	—	ReflectsColimits CategoryTheory.Functor.unop	—	reflectsColimitsOfShape_unop reflectsLimitsOfShape_of_reflectsLimits
reflectsFiniteColimits_leftOp 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsColimitsOfShape_leftOp ReflectsFiniteLimits.reflects
reflectsFiniteColimits_of_leftOp 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_leftOp ReflectsFiniteLimits.reflects
reflectsFiniteColimits_of_op 📖	mathematical	—	ReflectsFiniteColimits	—	reflectsColimitsOfShape_of_op ReflectsFiniteLimits.reflects
reflectsFiniteColimits_of_rightOp 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_rightOp ReflectsFiniteLimits.reflects
reflectsFiniteColimits_of_unop 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite	—	reflectsColimitsOfShape_of_unop ReflectsFiniteLimits.reflects
reflectsFiniteColimits_op 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsColimitsOfShape_op ReflectsFiniteLimits.reflects
reflectsFiniteColimits_rightOp 📖	mathematical	—	ReflectsFiniteColimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsColimitsOfShape_rightOp ReflectsFiniteLimits.reflects
reflectsFiniteColimits_unop 📖	mathematical	—	ReflectsFiniteColimits CategoryTheory.Functor.unop	—	reflectsColimitsOfShape_unop ReflectsFiniteLimits.reflects
reflectsFiniteCoproducts_leftOp 📖	mathematical	—	ReflectsFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsColimitsOfShape_leftOp reflectsLimitsOfShape_of_equiv instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite Finite.of_fintype
reflectsFiniteCoproducts_op 📖	mathematical	—	ReflectsFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsColimitsOfShape_op reflectsLimitsOfShape_of_equiv instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite Finite.of_fintype
reflectsFiniteCoproducts_rightOp 📖	mathematical	—	ReflectsFiniteCoproducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsColimitsOfShape_rightOp reflectsLimitsOfShape_of_equiv instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite Finite.of_fintype
reflectsFiniteCoproducts_unop 📖	mathematical	—	ReflectsFiniteCoproducts CategoryTheory.Functor.unop	—	reflectsColimitsOfShape_unop reflectsLimitsOfShape_of_equiv instReflectsLimitsOfShapeDiscreteOfReflectsFiniteProductsOfFinite Finite.of_fintype
reflectsFiniteLimits_leftOp 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsLimitsOfShape_leftOp ReflectsFiniteColimits.reflects
reflectsFiniteLimits_of_leftOp 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_leftOp ReflectsFiniteColimits.reflects
reflectsFiniteLimits_of_op 📖	mathematical	—	ReflectsFiniteLimits	—	reflectsLimitsOfShape_of_op ReflectsFiniteColimits.reflects
reflectsFiniteLimits_of_rightOp 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_rightOp ReflectsFiniteColimits.reflects
reflectsFiniteLimits_of_unop 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_unop ReflectsFiniteColimits.reflects
reflectsFiniteLimits_op 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsLimitsOfShape_op ReflectsFiniteColimits.reflects
reflectsFiniteLimits_rightOp 📖	mathematical	—	ReflectsFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsLimitsOfShape_rightOp ReflectsFiniteColimits.reflects
reflectsFiniteLimits_unop 📖	mathematical	—	ReflectsFiniteLimits CategoryTheory.Functor.unop	—	reflectsLimitsOfShape_unop ReflectsFiniteColimits.reflects
reflectsFiniteProducts_leftOp 📖	mathematical	—	ReflectsFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsLimitsOfShape_leftOp reflectsColimitsOfShape_of_equiv instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite Finite.of_fintype
reflectsFiniteProducts_op 📖	mathematical	—	ReflectsFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsLimitsOfShape_op reflectsColimitsOfShape_of_equiv instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite Finite.of_fintype
reflectsFiniteProducts_rightOp 📖	mathematical	—	ReflectsFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsLimitsOfShape_rightOp reflectsColimitsOfShape_of_equiv instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite Finite.of_fintype
reflectsFiniteProducts_unop 📖	mathematical	—	ReflectsFiniteProducts CategoryTheory.Functor.unop	—	reflectsLimitsOfShape_unop reflectsColimitsOfShape_of_equiv instReflectsColimitsOfShapeDiscreteOfReflectsFiniteCoproductsOfFinite Finite.of_fintype
reflectsLimit_leftOp 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
reflectsLimit_of_leftOp 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite	—	—
reflectsLimit_of_op 📖	mathematical	—	ReflectsLimit	—	—
reflectsLimit_of_rightOp 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite	—	—
reflectsLimit_of_unop 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite	—	—
reflectsLimit_op 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
reflectsLimit_rightOp 📖	mathematical	—	ReflectsLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
reflectsLimit_unop 📖	mathematical	—	ReflectsLimit CategoryTheory.Functor.unop	—	—
reflectsLimitsOfShape_leftOp 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsLimit_leftOp reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_of_leftOp 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsLimit_of_leftOp reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_of_op 📖	mathematical	—	ReflectsLimitsOfShape	—	reflectsLimit_of_op reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_of_rightOp 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsLimit_of_rightOp reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_of_unop 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite	—	reflectsLimit_of_unop reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_op 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsLimit_op reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_rightOp 📖	mathematical	—	ReflectsLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsLimit_rightOp reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfShape_unop 📖	mathematical	—	ReflectsLimitsOfShape CategoryTheory.Functor.unop	—	reflectsLimit_unop reflectsColimit_of_reflectsColimitsOfShape
reflectsLimitsOfSize_leftOp 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsLimitsOfShape_leftOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_of_leftOp 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_leftOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_of_op 📖	mathematical	—	ReflectsLimitsOfSize	—	reflectsLimitsOfShape_of_op reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_of_rightOp 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_rightOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_of_unop 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_unop reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_op 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsLimitsOfShape_op reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_rightOp 📖	mathematical	—	ReflectsLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsLimitsOfShape_rightOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimitsOfSize_unop 📖	mathematical	—	ReflectsLimitsOfSize CategoryTheory.Functor.unop	—	reflectsLimitsOfShape_unop reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_leftOp 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	reflectsLimitsOfShape_leftOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_of_leftOp 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_leftOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_of_op 📖	mathematical	—	ReflectsLimits	—	reflectsLimitsOfShape_of_op reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_of_rightOp 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_rightOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_of_unop 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite	—	reflectsLimitsOfShape_of_unop reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_op 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	reflectsLimitsOfShape_op reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_rightOp 📖	mathematical	—	ReflectsLimits Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	reflectsLimitsOfShape_rightOp reflectsColimitsOfShape_of_reflectsColimits
reflectsLimits_unop 📖	mathematical	—	ReflectsLimits CategoryTheory.Functor.unop	—	reflectsLimitsOfShape_unop reflectsColimitsOfShape_of_reflectsColimits

---

← Back to Index