smul_finset_union — Mathlib

English

For any α, β, γ, DecidableEq β, and SMul α β, and any Finsets s1, s2 ⊆ β, the scalar action distributes over union: a • (s1 ∪ s2) = (a • s1) ∪ (a • s2).

Русский

Пусть α действует на β, и имеется операция умножения на множества; распределение скаляра по объединению: a • (s1 ∪ s2) = a • s1 ∪ a • s2.

LaTeX

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

Lean4

@[to_additive]
theorem smul_finset_union : a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂ :=
  image_union _ _

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