smul — Mathlib

English

If HasSum f s and HasSum g t and Summable of the pointwise product, then HasSum (f x.1 • g x.2) (s • t).

Русский

Если HasSum f s и HasSum g t и есть суммируемость попарного произведения, тогда HasSum (f x.1 • g x.2) (s • t).

LaTeX

$$$$ \text{HasSum } f s \to \text{HasSum } g t \to \text{Summable } (\lambda x : \iota \times \kappa, f x.1 \cdot g x.2) \to \text{HasSum } (\lambda x, f x.1 \cdot g x.2) (s \cdot t). $$$$

Lean4

theorem smul (hf : HasSum f s) (hg : HasSum g t) (hfg : Summable fun x : ι × κ ↦ f x.1 • g x.2) :
    HasSum (fun x : ι × κ ↦ f x.1 • g x.2) (s • t) :=
  let ⟨_u, hu⟩ := hfg
  (hf.smul_eq hg hu).symm ▸ hu

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