Theorems · Theorem · category theory

CategoryTheory.Functor.WellOrderInductionData.map_succ

∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self : F.WellOrderInductionData) (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (self.succ j hj x) = x

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderSuccOrder