eqToHom

Mathlib.CategoryTheory.MorphismProperty.Composition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.ContainsIdentities.eqToHom

← MathLib Explorer

English

For W with identities, if h: x = y, then W(eqToHom h).

Русский

Для W с идентичностями, если h: x = y, то W(eqToHom h).

LaTeX

$$$W(\\operatorname{eqToHom} h)$$$

Lean4

theorem eqToHom (W : MorphismProperty C) [W.ContainsIdentities] {x y : C} (h : x = y) : W (eqToHom h) :=
  by
  subst h
  rw [eqToHom_refl]
  exact id_mem x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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