smul_union

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.smul_union

English

The product distributes over union on the right: 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₂ :=
  image2_union_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru