inv_whiskerLeft

Mathlib.CategoryTheory.Monoidal.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.inv_whiskerLeft

English

For X and an isomorphism f: Y ⟶ Z, inv (X ◁ f) = X ◁ inv f.

Русский

Для X и изоморфизма f: Y ⟶ Z, inv (X ◁ f) = X ◁ inv f.

LaTeX

$$$ \\mathrm{inv}(X \\triangleleft f) = X \\triangleleft \\mathrm{inv}(f) $$$

Lean4

@[simp]
theorem inv_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] : inv (X ◁ f) = X ◁ inv f := by cat_disch

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

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

Разделы

Аффилиация

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