instUnique

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.WellOrderInductionData.Extension.instUnique

English

For each j, the extension is unique (up to equality).

Русский

Для каждого j расширение уникально (с точностью до равенства).

LaTeX

$$$\\text{Unique}(d.Extension val_0 j)$$$

Lean4

noncomputable instance (j : J) : Unique (d.Extension val₀ j) :=
  uniqueOfSubsingleton (Nonempty.some inferInstance)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru