Theorems · Theorem · category theory
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext
∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
{x y : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ}, x.W = y.W → x.P = y.P → x = y- Cited by
- 2 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- Cardinalstatement and proof · cited by 2,598
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.SmallCategorystatement and proof · cited by 480
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagramstatement and proof · cited by 37
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.Pstatement and proof · cited by 28
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.Wstatement and proof · cited by 26
- CategoryTheory.MorphismProperty.HasCardinalLTproof · cited by 8
- CategoryTheory.ObjectProperty.HasCardinalLTproof · cited by 8
Cited by2
Results whose statement or proof uses this declaration.