Theorems · Theorem · category theory

CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective

∀ {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}
  {e e' : d.Extension val₀ j}, e.val = e'.val → e = e'

Defined in

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderOrderBot