cons_smul — Mathlib

English

A continuous multilinear map is homogeneous in the first variable: f(cons(c•x,m)) = c • f(cons(x,m)).

Русский

Отображение непрерывно мультилинейно по первой переменной однородно: f(cons(c·x,m)) = c·f(cons(x,m)).

LaTeX

$$$f(\mathrm{cons}(c\cdot x,m)) = c\cdot f(\mathrm{cons}(x,m)).$$$

Lean4

/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
multiplicativity of a multilinear map along the first variable. -/
theorem cons_smul (f : ContinuousMultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R) (x : M 0) :
    f (cons (c • x) m) = c • f (cons x m) :=
  f.toMultilinearMap.cons_smul m c x

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