mapL_apply — Mathlib

English

For any x in the tensor product ⨂ i, E i, applying mapL f to x is the same as applying the coordinatewise maps to x, i.e., mapL f x = map (i ↦ (f i).toLinearMap) x.

Русский

Для любого x в тензорном произведении ⨂ i, E_i применение mapL f к x даёт то же самое, что и применение координатных отображений: mapL f x = map (i ↦ (f i).toLinearMap) x.

LaTeX

$$$ x \\in \\bigotimes_{i} E_i \\quad \\Rightarrow \\quad mapL f\,x = map\\bigl( i \\mapsto (f i).toLinearMap \\bigr)\\,x $$$

Lean4

@[simp]
theorem mapL_apply (x : ⨂[𝕜] i, E i) : mapL f x = map (fun i ↦ (f i).toLinearMap) x := by rfl

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