union_smul — Mathlib

English

The scalar product of the union of two finite sets with t equals the union of their scalar products with t: (s1 ∪ s2) • t = (s1 • t) ∪ (s2 • t).

Русский

Умножение множества по скаляру через объединение: (s1 ∪ s2) • t = (s1 • t) ∪ (s2 • t).

LaTeX

$$$ (s_1 \cup s_2) \cdot t = (s_1 \cdot t) \cup (s_2 \cdot t) $$$

Lean4

@[to_additive]
theorem union_smul [DecidableEq α] : (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t :=
  image₂_union_left

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