mul — Mathlib

English

The product of summable families coincides with the bilinear smul of the same families.

Русский

Произведение суммируемых семейств совпадает с билинейным smul теми же семействами.

LaTeX

$$$ mul\ s t = smul\ s t $$$

Lean4

/-- A summable family given by pointwise multiplication of a pair of summable families. -/
@[simps]
def mul (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) : (SummableFamily Γ R (α × β))
    where
  toFun a := s (a.1) * t (a.2)
  isPWO_iUnion_support' := isPWO_iUnion_support_prod_mul s.isPWO_iUnion_support t.isPWO_iUnion_support
  finite_co_support' g := finite_co_support_prod_mul s t g

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