instHomIsOverId

Mathlib.CategoryTheory.Comma.Over.OverClass

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instHomIsOverId

English

There is an instance stating that the identity morphism is a HomOver morphism.

Русский

Существует инстанс, что тождественный морфизм является HomOver-морфизмом.

LaTeX

$$$\mathsf{HomIsOver}(\mathrm{id}_X,S)$$$

Lean4

instance [OverClass X S] : HomIsOver (𝟙 X) S where

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

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

Разделы

Аффилиация

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