piTensorHomMapFun₂_add — Mathlib

English

piTensorHomMapFun₂ maps a family of bilinear maps to a bilinear map between tensor products by composing with the tprod.

Русский

piTensorHomMapFun₂ переводит семейство билинейных отображений в билинейное отображение между тензорными произведениями через tprod.

LaTeX

$$$\pi\text{TensorHomMapFun₂} : (\otimes_i s_i \to t_i \to t'_i) \to (\otimes_i s_i \to \otimes_i t_i \to \otimes_i t'_i)$$$

Lean4

theorem piTensorHomMapFun₂_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) :
    piTensorHomMapFun₂ (φ + ψ) = piTensorHomMapFun₂ φ + piTensorHomMapFun₂ ψ := by dsimp [piTensorHomMapFun₂]; ext;
  simp only [map_add, LinearMap.compMultilinearMap_apply, lift.tprod, add_apply, LinearMap.add_apply]

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