Theorems · Inductive type · category theory

CategoryTheory.IsFiltered.filteredClosure

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {α : Type w} → (α → C) → CategoryTheory.ObjectProperty C

The "filtered closure" of an α-indexed family of objects in C is the set of objects in C obtained by starting with the family and successively adding maxima and coequalizers.

Defined in

Mathlib.CategoryTheory.Filtered.Small

Cited by

2 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredOrEmpty