Theorems · Definition · category theory
CategoryTheory.ObjectProperty.unop
{C : Type u} →
[inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty Cᵒᵖ → CategoryTheory.ObjectProperty CThe property of objects of C corresponding to P : ObjectProperty Cᵒᵖ.
- Cited by
- 29 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.
Cites3
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
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.CategoryStructstatement and proof · cited by 343
Cited by29
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.op_unopstatement · cited by 10
- CategoryTheory.ObjectProperty.unop_singletonstatement · cited by 4
- CategoryTheory.ObjectProperty.trW_of_unopstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.unop_monotonestatement 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.op_injectiveproof · cited by 2
- CategoryTheory.ObjectProperty.unop_injectivestatement and proof · cited by 1
- CategoryTheory.ObjectProperty.unop_isoClosurestatement and proof · cited by 1
- CategoryTheory.ObjectProperty.unop_ofObjstatement · cited by 1
- CategoryTheory.ObjectProperty.unop_opstatement · cited by 1
- CategoryTheory.ObjectProperty.isCodetecting_unop_iffstatement and proof · cited by 1