smul_right — Mathlib

English

If the supports of f_i are locally finite, then the supports of s_i · f_i are locally finite.

Русский

Если опоры функций f_i локально конечны, то опоры произведения f_i · s_i тоже локально конечны.

LaTeX

$$$\operatorname{LocallyFinite}(i \mapsto \operatorname{support}(f_i)) \Rightarrow \operatorname{LocallyFinite}\bigl(i \mapsto \operatorname{support}(s_i \cdot f_i)\bigr).$$$

Lean4

theorem smul_right [Zero M] [SMulZeroClass R M] {f : ι → X → M} (h : LocallyFinite fun i ↦ support <| f i)
    (s : ι → X → R) : LocallyFinite fun i ↦ support <| s i • f i :=
  h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]

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