Theorems · Inductive type · category theory
CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → PropA predicate C → Prop on the objects of a category is closed under isomorphisms
if whenever P X, then all the objects Y that are isomorphic to X also satisfy P Y.
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.ObjectPropertystatement · cited by 798
Cited by82
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.prop_of_isostatement and proof · cited by 23
- CategoryTheory.ObjectProperty.prop_iff_of_isostatement and proof · cited by 13
- CategoryTheory.ObjectProperty.isoClosure_eq_selfstatement and proof · cited by 12
- CategoryTheory.ObjectProperty.isoClosure_le_iffstatement and proof · cited by 8
- CategoryTheory.ObjectProperty.limitsClosure_lestatement and proof · cited by 6
- CategoryTheory.ObjectProperty.colimitsClosure_lestatement and proof · cited by 6
- CategoryTheory.ObjectProperty.shiftClosure_eq_selfstatement and proof · cited by 4
- CategoryTheory.ObjectProperty.trW_iff_of_distinguishedstatement and proof · cited by 4
- CategoryTheory.Equivalence.congrFullSubcategorystatement and proof · cited by 4
- CategoryTheory.ObjectProperty.prop_of_isZerostatement and proof · cited by 3
- AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphismsstatement and proof · cited by 3
- CategoryTheory.ObjectProperty.limitsClosure_eq_selfstatement and proof · cited by 2