tensorTensorTensorAssoc_tmul — Mathlib

English

The two ways of composing maps f,g,h with associator agree after transporting along the isomorphisms: map f (map g h) (assoc x) equals assoc (map (map f g) h x).

Русский

Два способа компоновки отображений f,g,h с использованием ассоциатора совпадают при переносе через изоморфизм.

LaTeX

$$$\\mathrm{map}\\;f\\; (\\mathrm{map}\\;g\\; h) (\\alpha_{M,N,P}(x)) = \\alpha_{Q,S,T}(\\mathrm{map}\\; (\\mathrm{map}\\;f\\; g)\\; h\\; x)$$$

Lean4

@[simp]
theorem tensorTensorTensorAssoc_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorAssoc R M N P Q (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q :=
  rfl

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