Theorems · Theorem · category theory

CategoryTheory.Limits.hasIterationOfShape_of_initialSeg

∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] {α : Type u_1}
  [inst_5 : LinearOrder α] (h : α ≤i J) [Nonempty α], CategoryTheory.Limits.HasIterationOfShape α C

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderCategoryTheory.CategoryCategoryTheory.Limits.HasIterationOfShapeSuccOrderWellFoundedLTLinearOrderNonempty