Theorems · Theorem · category theory

CategoryTheory.Limits.Bicone.IsBilimit.ext

∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  {x y : B.IsBilimit}, x.isLimit = y.isLimit → x.isColimit = y.isColimit → x = y

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Cited by: 1 results in Mathlib
Foundations: Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

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.Discretestatement · cited by 2,447
CategoryTheory.Limits.IsColimitstatement and proof · cited by 773
CategoryTheory.Limits.IsLimitstatement and proof · cited by 664
CategoryTheory.Discrete.functorstatement · cited by 633
CategoryTheory.Limits.Biconestatement and proof · cited by 75
CategoryTheory.Limits.Bicone.IsBilimitstatement and proof · cited by 18
CategoryTheory.Limits.Bicone.toConestatement and proof · cited by 17
CategoryTheory.Limits.Bicone.toCoconestatement and proof · cited by 15
CategoryTheory.Limits.Bicone.IsBilimit.isLimitstatement and proof · cited by 9
CategoryTheory.Limits.Bicone.IsBilimit.isColimitstatement and proof · cited by 6

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Bicone.IsBilimit.ext_iffproof · cited by 0