Theorems · Definition · category theory
CategoryTheory.ObjectProperty.op
{C : Type u} →
[inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty CᵒᵖThe property of objects of Cᵒᵖ corresponding to P : ObjectProperty C.
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Oppositestatement and proof · cited by 8,081
- Opposite.unopproof · cited by 2,231
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.CategoryStructstatement and proof · cited by 343
Cited by44
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.op_unopstatement · cited by 10
- CategoryTheory.ObjectProperty.op_monotone_iffstatement · cited by 6
- CategoryTheory.ObjectProperty.opEquivalencestatement and proof · cited by 5
- CategoryTheory.ObjectProperty.op_singletonstatement · cited by 4
- CategoryTheory.ObjectProperty.isCoseparating_op_iffstatement and proof · cited by 3
- CategoryTheory.ObjectProperty.trW_of_opstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShapestatement and proof · cited by 2
- CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShapestatement and proof · cited by 2
- CategoryTheory.ObjectProperty.isCodetecting_op_iffstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.isDetecting_op_iffstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.isSeparating_op_iffstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.op_injectivestatement and proof · cited by 2