English
The following equality holds on arbitrary x: map f (map g h) (TensorProduct.assoc x) = TensorProduct.assoc (map (map f g) h x).
Русский
Следующее равенство выполняется для любого x: map f (map g h) (assoc x) = assoc (map (map f g) h x).
LaTeX
$$$\\text{map }f\\; (\\text{map }g\\; h)\\; (\\alpha_{M,N,P}(x)) = \\alpha_{Q,S,T}\\; (\\text{map }(\\text{map }f g)\\; h)(x)$$$
Lean4
theorem map_map_assoc_symm (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : M ⊗[R] (N ⊗[R] P)) :
map (map f g) h ((TensorProduct.assoc R M N P).symm x) = (TensorProduct.assoc R Q S T).symm (map f (map g h) x) :=
DFunLike.congr_fun (map_map_comp_assoc_symm_eq _ _ _) _