Theorems · Definition · category theory

DirectLimit

{ι : Type u_1} →
  [inst : Preorder ι] →
    (F : ι → Type u_4) →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] → [IsDirectedOrder ι] → Type (max u_4 u_1)

The direct limit of a directed system.

Defined in

Mathlib.Order.DirectedInverseSystem

Cited by

103 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 31 definitions · uses no axioms

Assumes

PreorderFunLikeDirectedSystemIsDirectedOrder