map_coord_zero — Mathlib

English

Let f be a continuous multilinear map. If the i-th coordinate of m is zero, then f(m) = 0.

Русский

Пусть f — непрерывная многочередная карта. Если i-я координата m равна нулю, то f(m) = 0.

LaTeX

$$$\\forall i, \\forall m: (\\forall j, M_{1}(j)),\\; m(i)=0 \\Rightarrow f(m)=0.$$$

Lean4

theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0 :=
  f.toMultilinearMap.map_coord_zero i h

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