applyAddHom — Mathlib

English

Combine a family of continuous multilinear maps f_i with domain M₁ into a map into the function space ∀ i, M' i, with evaluation given by the pi construction.

Русский

Объединяем семейство отображений через pi в отображение в пространство функций.

LaTeX

$$$\\text{pi } f: M_1 \\to \\forall i, M' i.$$$

Lean4

/-- Evaluation of a `ContinuousMultilinearMap` at a vector as an `AddMonoidHom`. -/
def applyAddHom (m : ∀ i, M₁ i) : ContinuousMultilinearMap R M₁ M₂ →+ M₂
    where
  toFun f := f m
  map_zero' := rfl
  map_add' _ _ := rfl

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