objIso

Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso

English

There is a family of isomorphisms between obj c i and F.obj ⟨i, hi⟩ for i<j.

Русский

Для каждого i<j существует изоморфизм между obj c i и F.obj ⟨i, hi⟩.

LaTeX

$$$\\text{ofCocone.objIso} (i) (hi) : \\text{obj} \\; c \\; i \\cong F.obj ⟨i, hi⟩$$$

Lean4

/-- Auxiliary definition for `ofCocone`. -/
def objIso (i : J) (hi : i < j) : obj c i ≅ F.obj ⟨i, hi⟩ :=
  eqToIso (dif_pos hi)

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

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

Разделы

Аффилиация

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