tensorμ_snd

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianMonoidalCategory.tensorμ_snd

← MathLib Explorer

English

Similarly, fst and snd satisfy the μ-part: snd(W⊗Y, X⊗Z) = snd(W,X) ⊗ snd(Y,Z).

Русский

Аналогично: snd(W⊗Y, X⊗Z) = snd(W,X) ⊗ snd(Y,Z).

LaTeX

$$$tensor\mu\; W\; X\; Y\; Z \;≔\; snd(W\otimes Y, X\otimes Z) = snd(W,X) \otimes_{m} snd(Y,Z)$$$

Lean4

@[reassoc (attr := simp)]
theorem tensorμ_snd (W X Y Z : C) : tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z) = snd W X ⊗ₘ snd Y Z := by
  ext <;> simp [tensorμ]

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

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

Разделы

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

Аффилиация

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