Theorems · Theorem · category theory
CategoryTheory.isCoseparator_prod
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
[inst_2 : CategoryTheory.Limits.HasBinaryProduct G H],
CategoryTheory.IsCoseparator (G ⨯ H) ↔ (CategoryTheory.ObjectProperty.pair G H).IsCoseparating- Defined in
- Mathlib.CategoryTheory.Generator.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Limits.WalkingPairproof · cited by 1,319
- CategoryTheory.ObjectPropertyproof · cited by 798
- CategoryTheory.Limits.prodstatement · cited by 364
- CategoryTheory.Limits.HasBinaryProductstatement and proof · cited by 169
- CategoryTheory.Limits.WalkingPair.casesOnproof · cited by 59
- CategoryTheory.ObjectProperty.ofObjproof · cited by 37
- CategoryTheory.IsCoseparatorstatement · cited by 28
- CategoryTheory.ObjectProperty.IsCoseparatingstatement and proof · cited by 28
- CategoryTheory.Limits.prodIsProdproof · cited by 7
- CategoryTheory.ObjectProperty.pairstatement and proof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.isCoseparator_prod_of_isCoseparator_leftproof · cited by 0
- CategoryTheory.isCoseparator_prod_of_isCoseparator_rightproof · cited by 0