Theorems · Definition · category theory

CategoryTheory.IsCardinalFiltered.toMax

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [inst_1 : CategoryTheory.IsCardinalFiltered J κ] →
          {K : Type u'} →
            (S : K → J) → (hS : HasCardinalLT K κ) → (k : K) → S k ⟶ CategoryTheory.IsCardinalFiltered.max S hS

If S : K → J is a family of objects of cardinality < κ in a κ-filtered category, this is a choice of map S k ⟶ max S hS for any k : K.

Defined in

Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.IsCardinalFiltered