of_symmetric_monoidal_closed — Mathlib

English

If coprodComparison(tensorRight X) Y Z is an isomorphism for all X, Y, Z, then the monoidal category has right distributivity structure.

Русский

Если для всех X,Y,Z отображение coprodComparison(tensorRight X) Y Z является изоморфизмом, то существует правая распределительная структура.

LaTeX

$$$\\forall X,Y,Z, IsIso( coprodComparison (tensorRight X) Y Z) \\Rightarrow IsMonoidalRightDistrib C$$$

Lean4

instance of_symmetric_monoidal_closed [SymmetricCategory C] [MonoidalClosed C] : IsMonoidalDistrib C := by
  apply SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib

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