eHomWhiskerRight_id

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

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

English

Same as above: whiskering on the right by the identity yields identity.

Русский

Повторение: вправо взятие whisker от тождества даёт тождество.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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