Theorems · Definition · category theory

CategoryTheory.Functor.eventualRange

{J : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} J] →
    (F : CategoryTheory.Functor J (Type v)) → (j : J) → Set ((fun X => X) (F.obj j))

The eventual range of the functor F : J ⥤ Type v at index j : J is the intersection of the ranges of all maps F.map f with i : J and f : i ⟶ j.

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

13 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category