eHomWhiskerLeft_id

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

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

English

Whiskering on the left by identity yields identity in enriched Hom.

Русский

Слева взятое whisker от тождества даёт тождественный элемент в обогащённой Hom.

LaTeX

$$$eHomWhiskerLeft\,V\,X\,(\mathrm{Id}\,Y) = \mathrm{Id}\, _.$$$

Lean4

@[simp]
theorem eHomWhiskerLeft_id (X Y : C) : eHomWhiskerLeft V X (𝟙 Y) = 𝟙 _ := by simp [eHomWhiskerLeft]

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

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

Разделы

Аффилиация

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