Theorems · Theorem · category theory

CategoryTheory.IsCardinalFiltered.wideSpan

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ] {ι : Type v'} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i),
  HasCardinalLT ι κ → ∃ m a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) (a i) = b

Variant of IsFiltered.span for κ-filtered categories.

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered