domain_sup — Mathlib

English

Applying the sum of linear maps represented by a dependent finitely supported function to a vector b equals the sum over the indices of applying each map to b.

Русский

Применение суммы линейных отображений, заданной через dfinsupp, к вектору b эквивалентно сумме по индексам от применения каждого отображения к b.

LaTeX

$$$ (t.sum g)\, b = t.sum (\lambda i d, g i d b)$$$

Lean4

@[simp]
theorem domain_sup (f g : E →ₗ.[R] F) (h : ∀ (x : f.domain) (y : g.domain), (x : E) = y → f x = g y) :
    (f.sup g h).domain = f.domain ⊔ g.domain :=
  rfl

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