prod — Mathlib

English

The map toMultilinearMap preserves addition: (f+g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap.

Русский

toMultilinearMap сохраняет сложение: (f+g).toMultilinearMap = f.toMultilinearMap + g.toMultilinearMap.

LaTeX

$$$ (f+g)^{\\text{toMultilinearMap}} = f^{\\text{toMultilinearMap}} + g^{\\text{toMultilinearMap}} $$$

Lean4

/-- The Cartesian product of two continuous multilinear maps, as a continuous multilinear map. -/
def prod (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) :
    ContinuousMultilinearMap R M₁ (M₂ × M₃) :=
  { f.toMultilinearMap.prod g.toMultilinearMap with cont := f.cont.prodMk g.cont }

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