instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor

English

There exists a HasMap instance for the product-object construction induced by a trifunctor, i.e., the tensor of X1 and X2, mapped into X3, carries a HasMap structure compatible with p.

Русский

Существует экземпляр HasMap для конструкций произведения, индуцированной тройной функторной конструкцией; тензор X1 ⊗ X2 ⊗ X3 наследует структуру HasMap совместимую с p.

LaTeX

$$$\text{HasMap}(\mathrm{tensorObj}\, X_1 X_2, p) \Rightarrow \text{HasMap}(\mathrm{tensorObj}\, X_1 X_2, p)$$$

Lean4

instance (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃)
    [h : HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p] :
    HasMap (((mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃) p :=
  h

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