Theorems · Theorem · category theory

CategoryTheory.Functor.toPreimages_obj

∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) (j : J), (F.toPreimages s).obj j = ↑(⋂ f, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' s)

Defined in

Mathlib.CategoryTheory.CofilteredSystem

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category