Theorems · Theorem · category theory

CategoryTheory.Functor.eventualRange_eq_range_precomp

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j k : J}
  (f : i ⟶ j) (g : j ⟶ k),
  F.eventualRange k = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map g)) →
    F.eventualRange k =
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp f g)))

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category