Theorems · Definition · category theory

CategoryTheory.Functor.WellOrderInductionData.succ

{J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        F.WellOrderInductionData → (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))

A section F.obj (op j) → F.obj (op (Order.succ j)) to the restriction F.obj (op (Order.succ j)) → F.obj (op j) when j is not maximal.

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

7 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

LinearOrderSuccOrder