smul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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