Theorems · Theorem · category theory

CategoryTheory.Functor.mem_eventualRange_iff

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {j : J}
  {x : F.obj j},
  x ∈ F.eventualRange j ↔ ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category