Theorems · Definition · category theory

CategoryTheory.IsFiltered.max

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

max j j' is an arbitrary choice of object to the right of both j and j', whose existence is ensured by IsFiltered.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

26 results in Mathlib

Foundations

Depth 9 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty