smul_union — Mathlib

English

A scalar action distributes over the union on the second factor: s • (t1 ∪ t2) = (s • t1) ∪ (s • t2).

Русский

Действие скаляра распределяется по объединению второй компоненты: s • (t1 ∪ t2) = s • t1 ∪ s • t2.

LaTeX

$$$s \cdot (t_1 \cup t_2) = (s \cdot t_1) \cup (s \cdot t_2)$$$

Lean4

@[to_additive]
theorem smul_union : s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂ :=
  image₂_union_right

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