Theorems · Theorem · category theory

CategoryTheory.IsCardinalFiltered.coeq_condition

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [inst_1 : CategoryTheory.IsCardinalFiltered J κ] {K : Type v'} {j j' : J} (f : K → (j ⟶ j')) (hK : HasCardinalLT K κ)
  (k : K),
  CategoryTheory.CategoryStruct.comp (f k) (CategoryTheory.IsCardinalFiltered.coeqHom f hK) =
    CategoryTheory.IsCardinalFiltered.toCoeq f hK

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered