Theorems · Theorem · category theory

CategoryTheory.Functor.WellOrderInductionData.succ.congr_simp

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

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

LinearOrderSuccOrder