Opposite

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Opposite.lean

Statistics

Metric	Count
Definitions `op`, `subtypeOpEquiv`, `unop`	3
Theorems `instIsClosedUnderIsomorphismsOppositeOp`, `instIsClosedUnderIsomorphismsUnopOfOpposite`, `op_iff`, `op_injective`, `op_injective_iff`, `op_isoClosure`, `op_monotone`, `op_monotone_iff`, `op_ofObj`, `op_singleton`, `op_unop`, `unop_iff`, `unop_injective`, `unop_injective_iff`, `unop_isoClosure`, `unop_monotone`, `unop_monotone_iff`, `unop_ofObj`, `unop_op`, `unop_singleton`	20
Total	23

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`op` 📖	CompOp	43 math math: `colimitsOfShape_op`, `isClosedUnderColimitsOfShape_iff_op`, `CategoryTheory.isSeparating_unop_iff`, `instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape`, `isDetecting_op_iff`, `instContainsZeroOppositeOp`, `isCoseparating_op_iff`, `limitsOfShape_op`, `CategoryTheory.isSeparating_op_iff`, `op_monotone_iff`, `instIsClosedUnderIsomorphismsOppositeOp`, `InheritedFromTarget.op`, `CategoryTheory.isCoseparating_op_iff`, `op_singleton`, `instSmallOppositeOp`, `instSmallOppositeOp_1`, `instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1`, `op_iff`, `op_ofObj`, `limitsOfShape_eq_unop_colimitsOfShape`, `op_injective_iff`, `op_monotone`, `colimitsClosure_eq_unop_limitsClosure`, `instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape`, `CategoryTheory.isCodetecting_op_iff`, `CategoryTheory.isCoseparating_unop_iff`, `unop_op`, `instEssentiallySmallOppositeOp`, `instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1`, `InheritedFromSource.op`, `CategoryTheory.isDetecting_op_iff`, `isClosedUnderColimitsOfShape_op_iff_op`, `op_isoClosure`, `isClosedUnderLimitsOfShape_op_iff_op`, `isCodetecting_op_iff`, `isSeparating_op_iff`, `colimitsOfShape_eq_unop_limitsOfShape`, `CategoryTheory.isDetecting_unop_iff`, `op_unop`, `CategoryTheory.isCodetecting_unop_iff`, `essentiallySmall_op_iff`, `small_op_iff`, `isClosedUnderLimitsOfShape_iff_op`
`subtypeOpEquiv` 📖	CompOp	—
`unop` 📖	CompOp	31 math math: `instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape`, `instSmallUnopOfOpposite_1`, `essentiallySmall_unop_iff`, `unop_ofObj`, `unop_injective_iff`, `instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape`, `unop_isoClosure`, `isClosedUnderLimitsOfShape_op_iff_unop`, `isSeparating_unop_iff`, `isDetecting_unop_iff`, `instIsClosedUnderIsomorphismsUnopOfOpposite`, `instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite`, `isClosedUnderColimitsOfShape_op_iff_unop`, `limitsOfShape_eq_unop_colimitsOfShape`, `colimitsClosure_eq_unop_limitsClosure`, `unop_monotone_iff`, `instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite`, `isCoseparating_unop_iff`, `isCodetecting_unop_iff`, `unop_op`, `unop_iff`, `isClosedUnderColimitsOfShape_iff_unop`, `colimitsOfShape_eq_unop_limitsOfShape`, `unop_monotone`, `op_unop`, `small_unop_iff`, `instEssentiallySmallUnopOfOpposite`, `isClosedUnderLimitsOfShape_iff_unop`, `instContainsZeroUnopOfOpposite`, `unop_singleton`, `instSmallUnopOfOpposite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderIsomorphismsOppositeOp` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct`	—	`prop_of_iso`
`instIsClosedUnderIsomorphismsUnopOfOpposite` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `unop` `CategoryTheory.Category.toCategoryStruct`	—	`prop_of_iso`
`op_iff` 📖	mathematical	—	`op` `Opposite.unop`	—	—
`op_injective` 📖	—	`op`	—	—	`unop_op`
`op_injective_iff` 📖	mathematical	—	`op`	—	`op_injective`
`op_isoClosure` 📖	mathematical	—	`op` `CategoryTheory.Category.toCategoryStruct` `isoClosure` `Opposite` `CategoryTheory.Category.opposite`	—	—
`op_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `Pi.hasLe` `Prop.le`	`Opposite` `CategoryTheory.CategoryStruct.opposite` `op`	—	—
`op_monotone_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Pi.hasLe` `Prop.le` `op`	—	`unop_monotone` `op_monotone`
`op_ofObj` 📖	mathematical	—	`op` `ofObj` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Opposite.op`	—	—
`op_singleton` 📖	mathematical	—	`op` `singleton` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Opposite.op`	—	`op_ofObj`
`op_unop` 📖	mathematical	—	`op` `unop`	—	—
`unop_iff` 📖	mathematical	—	`unop` `Opposite.op`	—	—
`unop_injective` 📖	—	`unop`	—	—	`op_unop`
`unop_injective_iff` 📖	mathematical	—	`unop`	—	`unop_injective`
`unop_isoClosure` 📖	mathematical	—	`unop` `CategoryTheory.Category.toCategoryStruct` `isoClosure` `Opposite` `CategoryTheory.Category.opposite`	—	`op_injective_iff` `op_isoClosure` `op_unop`
`unop_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Pi.hasLe` `Prop.le`	`unop`	—	—
`unop_monotone_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `Pi.hasLe` `Prop.le` `unop` `Opposite` `CategoryTheory.CategoryStruct.opposite`	—	`op_monotone` `unop_monotone`
`unop_ofObj` 📖	mathematical	—	`unop` `ofObj` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Opposite.unop`	—	`op_injective` `op_ofObj`
`unop_op` 📖	mathematical	—	`unop` `op`	—	—
`unop_singleton` 📖	mathematical	—	`unop` `singleton` `Opposite` `CategoryTheory.CategoryStruct.opposite` `Opposite.unop`	—	`unop_ofObj`

---

← Back to Index