toLinearMap₁₂ — Mathlib

English

The map L.toLinearMap12 is the same bilinear map as L when evaluated at a pair (v,w); i.e., (L.toLinearMap12) v w = L v w.

Русский

Пусть L ∈ E →SL[σ1 3] F →SL[σ2 3] G; тогда (L.toLinearMap12) v w = L v w для любых v ∈ E, w ∈ F.

LaTeX

$$$(L^{\\mathrm{toLinearMap}_{12}})(v)(w) = L(v,w)$$$

Lean4

/-- Send a continuous bilinear map to an abstract bilinear map (forgetting continuity). -/
def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G :=
  (coeLMₛₗ σ₂₃).comp L.toLinearMap

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