Theorems · Definition · category theory

CategoryTheory.Functor.WellOrderInductionData.Extension.val

{J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] → {val₀ : F.obj (Opposite.op ⊥)} → {j : J} → d.Extension val₀ j → F.obj (Opposite.op j)

An element in F.obj (op j), which, by restriction, induces elements in F.obj (op i) for all i ≤ j.

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

8 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

LinearOrderSuccOrderOrderBot