lift_fst_comp_snd_comp

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp

English

The lift of fst followed by g and snd followed by g' equals the tensor of g and g'.

Русский

Лифт fst ≫ g и snd ≫ g' равен тензору g ⊗ g'.

LaTeX

$$lift (fst _ _ ≫ g) (snd _ _ ≫ g') = g ⊗ₘ g'$$

Lean4

@[simp]
theorem lift_fst_comp_snd_comp {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) : lift (fst _ _ ≫ g) (snd _ _ ≫ g') = g ⊗ₘ g' :=
  by ext <;> simp

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

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

Разделы

Аффилиация

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