Theorems · Theorem · category theory
CategoryTheory.ObjectProperty.isoClosure_eq_self
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
[P.IsClosedUnderIsomorphisms], P.isoClosure = P- Cited by
- 12 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Isoproof · cited by 3,963
- le_antisymmproof · cited by 2,068
- CategoryTheory.Iso.symmproof · cited by 993
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.ObjectProperty.IsClosedUnderIsomorphismsstatement and proof · cited by 68
- CategoryTheory.ObjectProperty.isoClosurestatement and proof · cited by 61
- CategoryTheory.ObjectProperty.prop_of_isoproof · cited by 23
- CategoryTheory.ObjectProperty.le_isoClosureproof · cited by 20
Cited by12
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.isoClosure_le_iffproof · cited by 8
- CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentableproof · cited by 1
- CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂proof · cited by 1
- CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'proof · cited by 0
- CategoryTheory.ObjectProperty.IsTriangulatedClosed₂.mk'proof · cited by 0
- CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.mk'proof · cited by 0
- CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₁proof · cited by 0
- CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₃proof · cited by 0
- CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk'proof · cited by 0
- CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.mk'proof · cited by 0