Theorems · Definition · category theory

CategoryTheory.IsCofiltered.min

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.IsCofilteredOrEmpty C] → C → C → C

min j j' is an arbitrary choice of object to the left of both j and j', whose existence is ensured by IsCofiltered.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

8 results in Mathlib

Foundations

Depth 9 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredOrEmpty