union_vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.union_vsub

English

The vsub distributes over union: (s1 ∪ s2) -ᵥ t = (s1 -ᵥ t) ∪ (s2 -ᵥ t).

Русский

VSub распределяется по объединению: (s1 ∪ s2) -ᵥ t = (s1 -ᵥ t) ∪ (s2 -ᵥ t).

LaTeX

$$$ (s_1 \cup s_2) -ᵥ t = (s_1 -ᵥ t) \cup (s_2 -ᵥ t) $$$

Lean4

theorem union_vsub : s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t) :=
  image₂_union_left

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

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

Разделы

Аффилиация

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