Theorems · Definition · category theory

CategoryTheory.Pairwise.cocone

{ι : Type v} →
  {α : Type u} →
    (U : ι → α) → [inst : CompleteLattice α] → CategoryTheory.Limits.Cocone (CategoryTheory.Pairwise.diagram U)

Given a function U : ι → α for [CompleteLattice α], iSup U provides a cocone over diagram U.

Defined in

Mathlib.CategoryTheory.Category.Pairwise

Cited by

8 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice