Theorems · Theorem · category theory

CategoryTheory.IsFilteredOrEmpty.cocone_objs

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] (X Y : C),
  ∃ Z x x, True

for every pair of objects there exists another object "to the right"

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.IsFilteredOrEmpty