Theorems · Theorem · category theory

CategoryTheory.SmallObject.prop_iterationFunctor_map_succ

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (j : κ.ord.ToType),
  (CategoryTheory.SmallObject.succStruct I κ).prop
    ((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯))

Defined in

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactOrderBotCategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument