Theorems · Theorem · category theory
CategoryTheory.Discrete.ext
∀ {α : Type u₁} {x y : CategoryTheory.Discrete α}, x.as = y.as → x = y- Defined in
- Mathlib.CategoryTheory.Discrete.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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.Discretestatement and proof · cited by 2,447
- CategoryTheory.Discrete.asstatement and proof · cited by 269
Cited by11
Results whose statement or proof uses this declaration.
- CategoryTheory.constant_of_preserves_morphismsproof · cited by 3
- CategoryTheory.IsPreconnected.of_constant_of_preserves_morphismsproof · cited by 2
- CategoryTheory.any_functor_const_on_objproof · cited by 1
- CategoryTheory.isPullback_initial_to_of_cofan_isVanKampenproof · cited by 1
- CategoryTheory.MorphismProperty.le_colimitsOfShape_punitproof · cited by 1
- CategoryTheory.FreeBicategory.preinclusion_map₂statement · cited by 0
- CategoryTheory.Discrete.ext_iffproof · cited by 0
- CategoryTheory.FreeMonoidalCategory.normalize_naturalitystatement and proof · cited by 0
- CategoryTheory.LocallyDiscrete.eq_of_homproof · cited by 0
- CategoryTheory.FreeBicategory.normalize_naturalitystatement and proof · cited by 0
- CategoryTheory.FreeMonoidalCategory.inclusion_mapstatement · cited by 0