eq_whisker

Mathlib.Tactic.CategoryTheory.IsoReassoc

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.eq_whisker

Lean4

theorem eq_whisker {C : Type*} [Category C] {X Y : C} {f g : X ≅ Y} (w : f = g) {Z : C} (h : Y ≅ Z) : f ≪≫ h = g ≪≫ h :=
  by rw [w]

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

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

Разделы

Аффилиация

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