objIsoPt

Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

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

English

The auxiliary iso between obj c j and c.pt is given by short-circuit choice of hi.

Русский

Вспомогательный изоморфизм между obj c j и c.pt задаётся выбором hi.

LaTeX

$$$\\text{ofCocone.objIsoPt} : obj c j \\cong c.pt$$$

Lean4

/-- Auxiliary definition for `ofCocone`. -/
def objIsoPt : obj c j ≅ c.pt :=
  eqToIso (dif_neg (by simp))

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

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

Разделы

Аффилиация

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