compMultilinearMap_apply — Mathlib

English

For any input m, evaluating the composed map equals applying f to m and then applying g to the result: (g ∘ f)(m) = g(f(m)).

Русский

При любом аргументе m значение композиции равно применению f к m, затем применения g к результату: (g ∘ f)(m) = g(f(m)).

LaTeX

$$$$(g\circ f)(m)=g(f(m)),$$ for all $m$ in the domain.$$

Lean4

@[simp]
theorem compMultilinearMap_apply (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (m : ∀ i, M₁ i) :
    g.compMultilinearMap f m = g (f m) :=
  rfl

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